H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 15.424 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule Main

((floor :: Float -> Int) :: Float -> Int)

module Main where

import qualified Prelude

Lambda Reductions:
The following Lambda expression

\(_,r)→r

is transformed to

r0 (_,r) = r

The following Lambda expression

\(n,_)→n

is transformed to

n0 (n,_) = n

The following Lambda expression

\(_,r)→r

is transformed to

r1 (_,r) = r

The following Lambda expression

\(q,_)→q

is transformed to

q1 (q,_) = q

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

mainModule Main

((floor :: Float -> Int) :: Float -> Int)

module Main where

import qualified Prelude

If Reductions:
The following If expression

if r < 0 then n - 1 else n

is transformed to

floor0 True = n - 1

floor0 False = n

The following If expression

if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to

primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))

primDivNatS0 x y False = Zero

The following If expression

if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to

primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)

primModNatS0 x y False = Succ x

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

mainModule Main

((floor :: Float -> Int) :: Float -> Int)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern

frac@(Double vz wu)

is replaced by the following term

Double vz wu

The bind variable of the following binding Pattern

frac@(Float wx wy)

is replaced by the following term

Float wx wy

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

mainModule Main

((floor :: Float -> Int) :: Float -> Int)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

mainModule Main

((floor :: Float -> Int) :: Float -> Int)

module Main where

import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

floor0 (r < 0)

where

floor0 True = n - 1

floor0 False = n

n = n0 vu9

n0 (n,vw) = n

r = r0 vu9

r0 (vv,r) = r

vu9 = properFraction x

are unpacked to the following functions on top level

floorVu9 xx = properFraction xx

floorR xx = floorR0 xx (floorVu9 xx)

floorN0 xx (n,vw) = n

floorR0 xx (vv,r) = r

floorN xx = floorN0 xx (floorVu9 xx)

floorFloor0 xx True = floorN xx - 1

floorFloor0 xx False = floorN xx

The bindings of the following Let/Where expression

(fromIntegral q,r :% y)

where

q = q1 vu30

q1 (q,xu) = q

r = r1 vu30

r1 (xv,r) = r

vu30 = quotRem x y

are unpacked to the following functions on top level

properFractionQ xy xz = properFractionQ1 xy xz (properFractionVu30 xy xz)

properFractionQ1 xy xz (q,xu) = q

properFractionVu30 xy xz = quotRem xy xz

properFractionR xy xz = properFractionR1 xy xz (properFractionVu30 xy xz)

properFractionR1 xy xz (xv,r) = r

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

mainModule Main

((floor :: Float -> Int) :: Float -> Int)

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

mainModule Main

(floor :: Float -> Int)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="floor",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="floor yu3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="floorFloor0 yu3 (floorR yu3 < fromInt (Pos Zero))",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="floorFloor0 yu3 (compare (floorR yu3) (fromInt (Pos Zero)) == LT)",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="floorFloor0 yu3 (primCmpFloat (floorR yu3) (fromInt (Pos Zero)) == LT)",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="floorFloor0 yu3 (primCmpFloat (floorR0 yu3 (floorVu9 yu3)) (fromInt (Pos Zero)) == LT)",fontsize=16,color="black",shape="box"];7 -> 8[label="",style="solid", color="black", weight=3];
8[label="floorFloor0 yu3 (primCmpFloat (floorR0 yu3 (properFraction yu3)) (fromInt (Pos Zero)) == LT)",fontsize=16,color="black",shape="box"];8 -> 9[label="",style="solid", color="black", weight=3];
9[label="floorFloor0 yu3 (primCmpFloat (floorR0 yu3 (floatProperFractionFloat yu3)) (fromInt (Pos Zero)) == LT)",fontsize=16,color="burlywood",shape="box"];5578[label="yu3/Float yu30 yu31",fontsize=10,color="white",style="solid",shape="box"];9 -> 5578[label="",style="solid", color="burlywood", weight=9];
5578 -> 10[label="",style="solid", color="burlywood", weight=3];
10[label="floorFloor0 (Float yu30 yu31) (primCmpFloat (floorR0 (Float yu30 yu31) (floatProperFractionFloat (Float yu30 yu31))) (fromInt (Pos Zero)) == LT)",fontsize=16,color="black",shape="box"];10 -> 11[label="",style="solid", color="black", weight=3];
11[label="floorFloor0 (Float yu30 yu31) (primCmpFloat (floorR0 (Float yu30 yu31) (fromInt (yu30 `quot` yu31),Float yu30 yu31 - fromInt (yu30 `quot` yu31))) (fromInt (Pos Zero)) == LT)",fontsize=16,color="black",shape="box"];11 -> 12[label="",style="solid", color="black", weight=3];
12[label="floorFloor0 (Float yu30 yu31) (primCmpFloat (Float yu30 yu31 - fromInt (yu30 `quot` yu31)) (fromInt (Pos Zero)) == LT)",fontsize=16,color="black",shape="box"];12 -> 13[label="",style="solid", color="black", weight=3];
13[label="floorFloor0 (Float yu30 yu31) (primCmpFloat (primMinusFloat (Float yu30 yu31) (fromInt (yu30 `quot` yu31))) (fromInt (Pos Zero)) == LT)",fontsize=16,color="black",shape="box"];13 -> 14[label="",style="solid", color="black", weight=3];
14[label="floorFloor0 (Float yu30 yu31) (primCmpFloat (primMinusFloat (Float yu30 yu31) (primIntToFloat (yu30 `quot` yu31))) (fromInt (Pos Zero)) == LT)",fontsize=16,color="black",shape="box"];14 -> 15[label="",style="solid", color="black", weight=3];
15[label="floorFloor0 (Float yu30 yu31) (primCmpFloat (primMinusFloat (Float yu30 yu31) (Float (yu30 `quot` yu31) (Pos (Succ Zero)))) (fromInt (Pos Zero)) == LT)",fontsize=16,color="black",shape="box"];15 -> 16[label="",style="solid", color="black", weight=3];
16[label="floorFloor0 (Float yu30 yu31) (primCmpFloat (Float (yu30 - yu30 `quot` yu31) (yu31 * Pos (Succ Zero))) (fromInt (Pos Zero)) == LT)",fontsize=16,color="black",shape="box"];16 -> 17[label="",style="solid", color="black", weight=3];
17[label="floorFloor0 (Float yu30 yu31) (primCmpFloat (Float (yu30 - yu30 `quot` yu31) (yu31 * Pos (Succ Zero))) (primIntToFloat (Pos Zero)) == LT)",fontsize=16,color="black",shape="box"];17 -> 18[label="",style="solid", color="black", weight=3];
18[label="floorFloor0 (Float yu30 yu31) (primCmpFloat (Float (yu30 - yu30 `quot` yu31) (yu31 * Pos (Succ Zero))) (Float (Pos Zero) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];18 -> 19[label="",style="solid", color="black", weight=3];
19[label="floorFloor0 (Float yu30 yu31) (compare ((yu30 - yu30 `quot` yu31) * Pos Zero) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];19 -> 20[label="",style="solid", color="black", weight=3];
20[label="floorFloor0 (Float yu30 yu31) (primCmpInt ((yu30 - yu30 `quot` yu31) * Pos Zero) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];20 -> 21[label="",style="solid", color="black", weight=3];
21[label="floorFloor0 (Float yu30 yu31) (primCmpInt (primMulInt (yu30 - yu30 `quot` yu31) (Pos Zero)) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];21 -> 22[label="",style="solid", color="black", weight=3];
22[label="floorFloor0 (Float yu30 yu31) (primCmpInt (primMulInt (primMinusInt yu30 (yu30 `quot` yu31)) (Pos Zero)) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="burlywood",shape="box"];5579[label="yu30/Pos yu300",fontsize=10,color="white",style="solid",shape="box"];22 -> 5579[label="",style="solid", color="burlywood", weight=9];
5579 -> 23[label="",style="solid", color="burlywood", weight=3];
5580[label="yu30/Neg yu300",fontsize=10,color="white",style="solid",shape="box"];22 -> 5580[label="",style="solid", color="burlywood", weight=9];
5580 -> 24[label="",style="solid", color="burlywood", weight=3];
23[label="floorFloor0 (Float (Pos yu300) yu31) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (Pos yu300 `quot` yu31)) (Pos Zero)) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];23 -> 25[label="",style="solid", color="black", weight=3];
24[label="floorFloor0 (Float (Neg yu300) yu31) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (Neg yu300 `quot` yu31)) (Pos Zero)) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];24 -> 26[label="",style="solid", color="black", weight=3];
25[label="floorFloor0 (Float (Pos yu300) yu31) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (primQuotInt (Pos yu300) yu31)) (Pos Zero)) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="burlywood",shape="box"];5581[label="yu31/Pos yu310",fontsize=10,color="white",style="solid",shape="box"];25 -> 5581[label="",style="solid", color="burlywood", weight=9];
5581 -> 27[label="",style="solid", color="burlywood", weight=3];
5582[label="yu31/Neg yu310",fontsize=10,color="white",style="solid",shape="box"];25 -> 5582[label="",style="solid", color="burlywood", weight=9];
5582 -> 28[label="",style="solid", color="burlywood", weight=3];
26[label="floorFloor0 (Float (Neg yu300) yu31) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (primQuotInt (Neg yu300) yu31)) (Pos Zero)) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="burlywood",shape="box"];5583[label="yu31/Pos yu310",fontsize=10,color="white",style="solid",shape="box"];26 -> 5583[label="",style="solid", color="burlywood", weight=9];
5583 -> 29[label="",style="solid", color="burlywood", weight=3];
5584[label="yu31/Neg yu310",fontsize=10,color="white",style="solid",shape="box"];26 -> 5584[label="",style="solid", color="burlywood", weight=9];
5584 -> 30[label="",style="solid", color="burlywood", weight=3];
27[label="floorFloor0 (Float (Pos yu300) (Pos yu310)) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (primQuotInt (Pos yu300) (Pos yu310))) (Pos Zero)) (Pos yu310 * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="burlywood",shape="box"];5585[label="yu310/Succ yu3100",fontsize=10,color="white",style="solid",shape="box"];27 -> 5585[label="",style="solid", color="burlywood", weight=9];
5585 -> 31[label="",style="solid", color="burlywood", weight=3];
5586[label="yu310/Zero",fontsize=10,color="white",style="solid",shape="box"];27 -> 5586[label="",style="solid", color="burlywood", weight=9];
5586 -> 32[label="",style="solid", color="burlywood", weight=3];
28[label="floorFloor0 (Float (Pos yu300) (Neg yu310)) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (primQuotInt (Pos yu300) (Neg yu310))) (Pos Zero)) (Neg yu310 * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="burlywood",shape="box"];5587[label="yu310/Succ yu3100",fontsize=10,color="white",style="solid",shape="box"];28 -> 5587[label="",style="solid", color="burlywood", weight=9];
5587 -> 33[label="",style="solid", color="burlywood", weight=3];
5588[label="yu310/Zero",fontsize=10,color="white",style="solid",shape="box"];28 -> 5588[label="",style="solid", color="burlywood", weight=9];
5588 -> 34[label="",style="solid", color="burlywood", weight=3];
29[label="floorFloor0 (Float (Neg yu300) (Pos yu310)) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (primQuotInt (Neg yu300) (Pos yu310))) (Pos Zero)) (Pos yu310 * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="burlywood",shape="box"];5589[label="yu310/Succ yu3100",fontsize=10,color="white",style="solid",shape="box"];29 -> 5589[label="",style="solid", color="burlywood", weight=9];
5589 -> 35[label="",style="solid", color="burlywood", weight=3];
5590[label="yu310/Zero",fontsize=10,color="white",style="solid",shape="box"];29 -> 5590[label="",style="solid", color="burlywood", weight=9];
5590 -> 36[label="",style="solid", color="burlywood", weight=3];
30[label="floorFloor0 (Float (Neg yu300) (Neg yu310)) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (primQuotInt (Neg yu300) (Neg yu310))) (Pos Zero)) (Neg yu310 * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="burlywood",shape="box"];5591[label="yu310/Succ yu3100",fontsize=10,color="white",style="solid",shape="box"];30 -> 5591[label="",style="solid", color="burlywood", weight=9];
5591 -> 37[label="",style="solid", color="burlywood", weight=3];
5592[label="yu310/Zero",fontsize=10,color="white",style="solid",shape="box"];30 -> 5592[label="",style="solid", color="burlywood", weight=9];
5592 -> 38[label="",style="solid", color="burlywood", weight=3];
31[label="floorFloor0 (Float (Pos yu300) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (primQuotInt (Pos yu300) (Pos (Succ yu3100)))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];31 -> 39[label="",style="solid", color="black", weight=3];
32[label="floorFloor0 (Float (Pos yu300) (Pos Zero)) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (primQuotInt (Pos yu300) (Pos Zero))) (Pos Zero)) (Pos Zero * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];32 -> 40[label="",style="solid", color="black", weight=3];
33[label="floorFloor0 (Float (Pos yu300) (Neg (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (primQuotInt (Pos yu300) (Neg (Succ yu3100)))) (Pos Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];33 -> 41[label="",style="solid", color="black", weight=3];
34[label="floorFloor0 (Float (Pos yu300) (Neg Zero)) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (primQuotInt (Pos yu300) (Neg Zero))) (Pos Zero)) (Neg Zero * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];34 -> 42[label="",style="solid", color="black", weight=3];
35[label="floorFloor0 (Float (Neg yu300) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (primQuotInt (Neg yu300) (Pos (Succ yu3100)))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];35 -> 43[label="",style="solid", color="black", weight=3];
36[label="floorFloor0 (Float (Neg yu300) (Pos Zero)) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (primQuotInt (Neg yu300) (Pos Zero))) (Pos Zero)) (Pos Zero * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];36 -> 44[label="",style="solid", color="black", weight=3];
37[label="floorFloor0 (Float (Neg yu300) (Neg (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (primQuotInt (Neg yu300) (Neg (Succ yu3100)))) (Pos Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];37 -> 45[label="",style="solid", color="black", weight=3];
38[label="floorFloor0 (Float (Neg yu300) (Neg Zero)) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (primQuotInt (Neg yu300) (Neg Zero))) (Pos Zero)) (Neg Zero * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];38 -> 46[label="",style="solid", color="black", weight=3];
39[label="floorFloor0 (Float (Pos yu300) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (Pos (primDivNatS yu300 (Succ yu3100)))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];39 -> 47[label="",style="solid", color="black", weight=3];
40[label="floorFloor0 (Float (Pos yu300) (Pos Zero)) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (error [])) (Pos Zero)) (Pos Zero * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];40 -> 48[label="",style="solid", color="black", weight=3];
41[label="floorFloor0 (Float (Pos yu300) (Neg (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (Neg (primDivNatS yu300 (Succ yu3100)))) (Pos Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];41 -> 49[label="",style="solid", color="black", weight=3];
42[label="floorFloor0 (Float (Pos yu300) (Neg Zero)) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (error [])) (Pos Zero)) (Neg Zero * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];42 -> 50[label="",style="solid", color="black", weight=3];
43[label="floorFloor0 (Float (Neg yu300) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (Neg (primDivNatS yu300 (Succ yu3100)))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];43 -> 51[label="",style="solid", color="black", weight=3];
44[label="floorFloor0 (Float (Neg yu300) (Pos Zero)) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (error [])) (Pos Zero)) (Pos Zero * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];44 -> 52[label="",style="solid", color="black", weight=3];
45[label="floorFloor0 (Float (Neg yu300) (Neg (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (Pos (primDivNatS yu300 (Succ yu3100)))) (Pos Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];45 -> 53[label="",style="solid", color="black", weight=3];
46[label="floorFloor0 (Float (Neg yu300) (Neg Zero)) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (error [])) (Pos Zero)) (Neg Zero * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];46 -> 54[label="",style="solid", color="black", weight=3];
47[label="floorFloor0 (Float (Pos yu300) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat yu300 (primDivNatS yu300 (Succ yu3100))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="burlywood",shape="box"];5593[label="yu300/Succ yu3000",fontsize=10,color="white",style="solid",shape="box"];47 -> 5593[label="",style="solid", color="burlywood", weight=9];
5593 -> 55[label="",style="solid", color="burlywood", weight=3];
5594[label="yu300/Zero",fontsize=10,color="white",style="solid",shape="box"];47 -> 5594[label="",style="solid", color="burlywood", weight=9];
5594 -> 56[label="",style="solid", color="burlywood", weight=3];
48[label="error []",fontsize=16,color="red",shape="box"];49[label="floorFloor0 (Float (Pos yu300) (Neg (Succ yu3100))) (primCmpInt (primMulInt (Pos (primPlusNat yu300 (primDivNatS yu300 (Succ yu3100)))) (Pos Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];49 -> 57[label="",style="solid", color="black", weight=3];
50[label="error []",fontsize=16,color="red",shape="box"];51[label="floorFloor0 (Float (Neg yu300) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (primDivNatS yu300 (Succ yu3100)) yu300) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="burlywood",shape="box"];5595[label="yu300/Succ yu3000",fontsize=10,color="white",style="solid",shape="box"];51 -> 5595[label="",style="solid", color="burlywood", weight=9];
5595 -> 58[label="",style="solid", color="burlywood", weight=3];
5596[label="yu300/Zero",fontsize=10,color="white",style="solid",shape="box"];51 -> 5596[label="",style="solid", color="burlywood", weight=9];
5596 -> 59[label="",style="solid", color="burlywood", weight=3];
52[label="error []",fontsize=16,color="red",shape="box"];53[label="floorFloor0 (Float (Neg yu300) (Neg (Succ yu3100))) (primCmpInt (primMulInt (Neg (primPlusNat yu300 (primDivNatS yu300 (Succ yu3100)))) (Pos Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];53 -> 60[label="",style="solid", color="black", weight=3];
54[label="error []",fontsize=16,color="red",shape="box"];55[label="floorFloor0 (Float (Pos (Succ yu3000)) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (Succ yu3000) (primDivNatS (Succ yu3000) (Succ yu3100))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];55 -> 61[label="",style="solid", color="black", weight=3];
56[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat Zero (primDivNatS Zero (Succ yu3100))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];56 -> 62[label="",style="solid", color="black", weight=3];
57[label="floorFloor0 (Float (Pos yu300) (Neg (Succ yu3100))) (primCmpInt (Pos (primMulNat (primPlusNat yu300 (primDivNatS yu300 (Succ yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="burlywood",shape="box"];5597[label="yu300/Succ yu3000",fontsize=10,color="white",style="solid",shape="box"];57 -> 5597[label="",style="solid", color="burlywood", weight=9];
5597 -> 63[label="",style="solid", color="burlywood", weight=3];
5598[label="yu300/Zero",fontsize=10,color="white",style="solid",shape="box"];57 -> 5598[label="",style="solid", color="burlywood", weight=9];
5598 -> 64[label="",style="solid", color="burlywood", weight=3];
58[label="floorFloor0 (Float (Neg (Succ yu3000)) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (primDivNatS (Succ yu3000) (Succ yu3100)) (Succ yu3000)) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];58 -> 65[label="",style="solid", color="black", weight=3];
59[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (primDivNatS Zero (Succ yu3100)) Zero) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];59 -> 66[label="",style="solid", color="black", weight=3];
60[label="floorFloor0 (Float (Neg yu300) (Neg (Succ yu3100))) (primCmpInt (Neg (primMulNat (primPlusNat yu300 (primDivNatS yu300 (Succ yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="burlywood",shape="box"];5599[label="yu300/Succ yu3000",fontsize=10,color="white",style="solid",shape="box"];60 -> 5599[label="",style="solid", color="burlywood", weight=9];
5599 -> 67[label="",style="solid", color="burlywood", weight=3];
5600[label="yu300/Zero",fontsize=10,color="white",style="solid",shape="box"];60 -> 5600[label="",style="solid", color="burlywood", weight=9];
5600 -> 68[label="",style="solid", color="burlywood", weight=3];
61[label="floorFloor0 (Float (Pos (Succ yu3000)) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (Succ yu3000) (primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="burlywood",shape="box"];5601[label="yu3000/Succ yu30000",fontsize=10,color="white",style="solid",shape="box"];61 -> 5601[label="",style="solid", color="burlywood", weight=9];
5601 -> 69[label="",style="solid", color="burlywood", weight=3];
5602[label="yu3000/Zero",fontsize=10,color="white",style="solid",shape="box"];61 -> 5602[label="",style="solid", color="burlywood", weight=9];
5602 -> 70[label="",style="solid", color="burlywood", weight=3];
62[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat Zero Zero) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];62 -> 71[label="",style="solid", color="black", weight=3];
63[label="floorFloor0 (Float (Pos (Succ yu3000)) (Neg (Succ yu3100))) (primCmpInt (Pos (primMulNat (primPlusNat (Succ yu3000) (primDivNatS (Succ yu3000) (Succ yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];63 -> 72[label="",style="solid", color="black", weight=3];
64[label="floorFloor0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos (primMulNat (primPlusNat Zero (primDivNatS Zero (Succ yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];64 -> 73[label="",style="solid", color="black", weight=3];
65 -> 4873[label="",style="dashed", color="red", weight=0];
65[label="floorFloor0 (Float (Neg (Succ yu3000)) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100)) (Succ yu3000)) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="magenta"];65 -> 4874[label="",style="dashed", color="magenta", weight=3];
65 -> 4875[label="",style="dashed", color="magenta", weight=3];
65 -> 4876[label="",style="dashed", color="magenta", weight=3];
66[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat Zero Zero) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];66 -> 76[label="",style="solid", color="black", weight=3];
67[label="floorFloor0 (Float (Neg (Succ yu3000)) (Neg (Succ yu3100))) (primCmpInt (Neg (primMulNat (primPlusNat (Succ yu3000) (primDivNatS (Succ yu3000) (Succ yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];67 -> 77[label="",style="solid", color="black", weight=3];
68[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg (primMulNat (primPlusNat Zero (primDivNatS Zero (Succ yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];68 -> 78[label="",style="solid", color="black", weight=3];
69[label="floorFloor0 (Float (Pos (Succ (Succ yu30000))) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (Succ (Succ yu30000)) (primDivNatS0 (Succ yu30000) yu3100 (primGEqNatS (Succ yu30000) yu3100))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="burlywood",shape="box"];5604[label="yu3100/Succ yu31000",fontsize=10,color="white",style="solid",shape="box"];69 -> 5604[label="",style="solid", color="burlywood", weight=9];
5604 -> 79[label="",style="solid", color="burlywood", weight=3];
5605[label="yu3100/Zero",fontsize=10,color="white",style="solid",shape="box"];69 -> 5605[label="",style="solid", color="burlywood", weight=9];
5605 -> 80[label="",style="solid", color="burlywood", weight=3];
70[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (Succ Zero) (primDivNatS0 Zero yu3100 (primGEqNatS Zero yu3100))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="burlywood",shape="box"];5606[label="yu3100/Succ yu31000",fontsize=10,color="white",style="solid",shape="box"];70 -> 5606[label="",style="solid", color="burlywood", weight=9];
5606 -> 81[label="",style="solid", color="burlywood", weight=3];
5607[label="yu3100/Zero",fontsize=10,color="white",style="solid",shape="box"];70 -> 5607[label="",style="solid", color="burlywood", weight=9];
5607 -> 82[label="",style="solid", color="burlywood", weight=3];
71[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (primMulInt (Pos Zero) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];71 -> 83[label="",style="solid", color="black", weight=3];
72 -> 5120[label="",style="dashed", color="red", weight=0];
72[label="floorFloor0 (Float (Pos (Succ yu3000)) (Neg (Succ yu3100))) (primCmpInt (Pos (primMulNat (primPlusNat (Succ yu3000) (primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="magenta"];72 -> 5121[label="",style="dashed", color="magenta", weight=3];
72 -> 5122[label="",style="dashed", color="magenta", weight=3];
72 -> 5123[label="",style="dashed", color="magenta", weight=3];
73[label="floorFloor0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos (primMulNat (primPlusNat Zero Zero) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];73 -> 86[label="",style="solid", color="black", weight=3];
4874[label="yu3000",fontsize=16,color="green",shape="box"];4875 -> 4730[label="",style="dashed", color="red", weight=0];
4875[label="primMinusNat (primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100)) (Succ yu3000)",fontsize=16,color="magenta"];4875 -> 4878[label="",style="dashed", color="magenta", weight=3];
4875 -> 4879[label="",style="dashed", color="magenta", weight=3];
4876[label="yu3100",fontsize=16,color="green",shape="box"];4873[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (primMulInt yu453 (Pos Zero)) (Pos (Succ yu450) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];5610[label="yu453/Pos yu4530",fontsize=10,color="white",style="solid",shape="box"];4873 -> 5610[label="",style="solid", color="burlywood", weight=9];
5610 -> 4880[label="",style="solid", color="burlywood", weight=3];
5611[label="yu453/Neg yu4530",fontsize=10,color="white",style="solid",shape="box"];4873 -> 5611[label="",style="solid", color="burlywood", weight=9];
5611 -> 4881[label="",style="solid", color="burlywood", weight=3];
76[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (primMulInt (Pos Zero) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];76 -> 91[label="",style="solid", color="black", weight=3];
77 -> 5140[label="",style="dashed", color="red", weight=0];
77[label="floorFloor0 (Float (Neg (Succ yu3000)) (Neg (Succ yu3100))) (primCmpInt (Neg (primMulNat (primPlusNat (Succ yu3000) (primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="magenta"];77 -> 5141[label="",style="dashed", color="magenta", weight=3];
77 -> 5142[label="",style="dashed", color="magenta", weight=3];
77 -> 5143[label="",style="dashed", color="magenta", weight=3];
78[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg (primMulNat (primPlusNat Zero Zero) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];78 -> 94[label="",style="solid", color="black", weight=3];
79[label="floorFloor0 (Float (Pos (Succ (Succ yu30000))) (Pos (Succ (Succ yu31000)))) (primCmpInt (primMulInt (primMinusNat (Succ (Succ yu30000)) (primDivNatS0 (Succ yu30000) (Succ yu31000) (primGEqNatS (Succ yu30000) (Succ yu31000)))) (Pos Zero)) (Pos (Succ (Succ yu31000)) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];79 -> 95[label="",style="solid", color="black", weight=3];
80[label="floorFloor0 (Float (Pos (Succ (Succ yu30000))) (Pos (Succ Zero))) (primCmpInt (primMulInt (primMinusNat (Succ (Succ yu30000)) (primDivNatS0 (Succ yu30000) Zero (primGEqNatS (Succ yu30000) Zero))) (Pos Zero)) (Pos (Succ Zero) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];80 -> 96[label="",style="solid", color="black", weight=3];
81[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ (Succ yu31000)))) (primCmpInt (primMulInt (primMinusNat (Succ Zero) (primDivNatS0 Zero (Succ yu31000) (primGEqNatS Zero (Succ yu31000)))) (Pos Zero)) (Pos (Succ (Succ yu31000)) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];81 -> 97[label="",style="solid", color="black", weight=3];
82[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primCmpInt (primMulInt (primMinusNat (Succ Zero) (primDivNatS0 Zero Zero (primGEqNatS Zero Zero))) (Pos Zero)) (Pos (Succ Zero) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];82 -> 98[label="",style="solid", color="black", weight=3];
83[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (Pos (primMulNat Zero Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];83 -> 99[label="",style="solid", color="black", weight=3];
5121[label="yu3000",fontsize=16,color="green",shape="box"];5122 -> 5132[label="",style="dashed", color="red", weight=0];
5122[label="primPlusNat (Succ yu3000) (primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100))",fontsize=16,color="magenta"];5122 -> 5133[label="",style="dashed", color="magenta", weight=3];
5123[label="yu3100",fontsize=16,color="green",shape="box"];5120[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (primCmpInt (Pos (primMulNat yu474 Zero)) (Neg (Succ yu464) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];5614[label="yu474/Succ yu4740",fontsize=10,color="white",style="solid",shape="box"];5120 -> 5614[label="",style="solid", color="burlywood", weight=9];
5614 -> 5134[label="",style="solid", color="burlywood", weight=3];
5615[label="yu474/Zero",fontsize=10,color="white",style="solid",shape="box"];5120 -> 5615[label="",style="solid", color="burlywood", weight=9];
5615 -> 5135[label="",style="solid", color="burlywood", weight=3];
86[label="floorFloor0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos (primMulNat Zero Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];86 -> 104[label="",style="solid", color="black", weight=3];
4878[label="primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100)",fontsize=16,color="burlywood",shape="triangle"];5616[label="yu3000/Succ yu30000",fontsize=10,color="white",style="solid",shape="box"];4878 -> 5616[label="",style="solid", color="burlywood", weight=9];
5616 -> 4893[label="",style="solid", color="burlywood", weight=3];
5617[label="yu3000/Zero",fontsize=10,color="white",style="solid",shape="box"];4878 -> 5617[label="",style="solid", color="burlywood", weight=9];
5617 -> 4894[label="",style="solid", color="burlywood", weight=3];
4879[label="Succ yu3000",fontsize=16,color="green",shape="box"];4730[label="primMinusNat yu4140 yu4390",fontsize=16,color="burlywood",shape="triangle"];5618[label="yu4140/Succ yu41400",fontsize=10,color="white",style="solid",shape="box"];4730 -> 5618[label="",style="solid", color="burlywood", weight=9];
5618 -> 4742[label="",style="solid", color="burlywood", weight=3];
5619[label="yu4140/Zero",fontsize=10,color="white",style="solid",shape="box"];4730 -> 5619[label="",style="solid", color="burlywood", weight=9];
5619 -> 4743[label="",style="solid", color="burlywood", weight=3];
4880[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (primMulInt (Pos yu4530) (Pos Zero)) (Pos (Succ yu450) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];4880 -> 4895[label="",style="solid", color="black", weight=3];
4881[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (primMulInt (Neg yu4530) (Pos Zero)) (Pos (Succ yu450) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];4881 -> 4896[label="",style="solid", color="black", weight=3];
91[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (Pos (primMulNat Zero Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];91 -> 109[label="",style="solid", color="black", weight=3];
5141[label="yu3100",fontsize=16,color="green",shape="box"];5142[label="yu3000",fontsize=16,color="green",shape="box"];5143 -> 5132[label="",style="dashed", color="red", weight=0];
5143[label="primPlusNat (Succ yu3000) (primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100))",fontsize=16,color="magenta"];5143 -> 5151[label="",style="dashed", color="magenta", weight=3];
5143 -> 5152[label="",style="dashed", color="magenta", weight=3];
5140[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (primCmpInt (Neg (primMulNat yu476 Zero)) (Neg (Succ yu469) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];5621[label="yu476/Succ yu4760",fontsize=10,color="white",style="solid",shape="box"];5140 -> 5621[label="",style="solid", color="burlywood", weight=9];
5621 -> 5153[label="",style="solid", color="burlywood", weight=3];
5622[label="yu476/Zero",fontsize=10,color="white",style="solid",shape="box"];5140 -> 5622[label="",style="solid", color="burlywood", weight=9];
5622 -> 5154[label="",style="solid", color="burlywood", weight=3];
94[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg (primMulNat Zero Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];94 -> 114[label="",style="solid", color="black", weight=3];
95 -> 3065[label="",style="dashed", color="red", weight=0];
95[label="floorFloor0 (Float (Pos (Succ (Succ yu30000))) (Pos (Succ (Succ yu31000)))) (primCmpInt (primMulInt (primMinusNat (Succ (Succ yu30000)) (primDivNatS0 (Succ yu30000) (Succ yu31000) (primGEqNatS yu30000 yu31000))) (Pos Zero)) (Pos (Succ (Succ yu31000)) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="magenta"];95 -> 3066[label="",style="dashed", color="magenta", weight=3];
95 -> 3067[label="",style="dashed", color="magenta", weight=3];
95 -> 3068[label="",style="dashed", color="magenta", weight=3];
96 -> 3065[label="",style="dashed", color="red", weight=0];
96[label="floorFloor0 (Float (Pos (Succ (Succ yu30000))) (Pos (Succ Zero))) (primCmpInt (primMulInt (primMinusNat (Succ (Succ yu30000)) (primDivNatS0 (Succ yu30000) Zero True)) (Pos Zero)) (Pos (Succ Zero) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="magenta"];96 -> 3069[label="",style="dashed", color="magenta", weight=3];
96 -> 3070[label="",style="dashed", color="magenta", weight=3];
96 -> 3071[label="",style="dashed", color="magenta", weight=3];
97[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ (Succ yu31000)))) (primCmpInt (primMulInt (primMinusNat (Succ Zero) (primDivNatS0 Zero (Succ yu31000) False)) (Pos Zero)) (Pos (Succ (Succ yu31000)) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];97 -> 118[label="",style="solid", color="black", weight=3];
98[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primCmpInt (primMulInt (primMinusNat (Succ Zero) (primDivNatS0 Zero Zero True)) (Pos Zero)) (Pos (Succ Zero) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];98 -> 119[label="",style="solid", color="black", weight=3];
99[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];99 -> 120[label="",style="solid", color="black", weight=3];
5133 -> 4878[label="",style="dashed", color="red", weight=0];
5133[label="primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100)",fontsize=16,color="magenta"];5133 -> 5136[label="",style="dashed", color="magenta", weight=3];
5133 -> 5137[label="",style="dashed", color="magenta", weight=3];
5132[label="primPlusNat (Succ yu3000) yu475",fontsize=16,color="burlywood",shape="triangle"];5626[label="yu475/Succ yu4750",fontsize=10,color="white",style="solid",shape="box"];5132 -> 5626[label="",style="solid", color="burlywood", weight=9];
5626 -> 5138[label="",style="solid", color="burlywood", weight=3];
5627[label="yu475/Zero",fontsize=10,color="white",style="solid",shape="box"];5132 -> 5627[label="",style="solid", color="burlywood", weight=9];
5627 -> 5139[label="",style="solid", color="burlywood", weight=3];
5134[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (primCmpInt (Pos (primMulNat (Succ yu4740) Zero)) (Neg (Succ yu464) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5134 -> 5155[label="",style="solid", color="black", weight=3];
5135[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (primCmpInt (Pos (primMulNat Zero Zero)) (Neg (Succ yu464) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5135 -> 5156[label="",style="solid", color="black", weight=3];
104[label="floorFloor0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos Zero) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];104 -> 125[label="",style="solid", color="black", weight=3];
4893[label="primDivNatS0 (Succ yu30000) yu3100 (primGEqNatS (Succ yu30000) yu3100)",fontsize=16,color="burlywood",shape="box"];5628[label="yu3100/Succ yu31000",fontsize=10,color="white",style="solid",shape="box"];4893 -> 5628[label="",style="solid", color="burlywood", weight=9];
5628 -> 4906[label="",style="solid", color="burlywood", weight=3];
5629[label="yu3100/Zero",fontsize=10,color="white",style="solid",shape="box"];4893 -> 5629[label="",style="solid", color="burlywood", weight=9];
5629 -> 4907[label="",style="solid", color="burlywood", weight=3];
4894[label="primDivNatS0 Zero yu3100 (primGEqNatS Zero yu3100)",fontsize=16,color="burlywood",shape="box"];5630[label="yu3100/Succ yu31000",fontsize=10,color="white",style="solid",shape="box"];4894 -> 5630[label="",style="solid", color="burlywood", weight=9];
5630 -> 4908[label="",style="solid", color="burlywood", weight=3];
5631[label="yu3100/Zero",fontsize=10,color="white",style="solid",shape="box"];4894 -> 5631[label="",style="solid", color="burlywood", weight=9];
5631 -> 4909[label="",style="solid", color="burlywood", weight=3];
4742[label="primMinusNat (Succ yu41400) yu4390",fontsize=16,color="burlywood",shape="box"];5632[label="yu4390/Succ yu43900",fontsize=10,color="white",style="solid",shape="box"];4742 -> 5632[label="",style="solid", color="burlywood", weight=9];
5632 -> 4754[label="",style="solid", color="burlywood", weight=3];
5633[label="yu4390/Zero",fontsize=10,color="white",style="solid",shape="box"];4742 -> 5633[label="",style="solid", color="burlywood", weight=9];
5633 -> 4755[label="",style="solid", color="burlywood", weight=3];
4743[label="primMinusNat Zero yu4390",fontsize=16,color="burlywood",shape="box"];5634[label="yu4390/Succ yu43900",fontsize=10,color="white",style="solid",shape="box"];4743 -> 5634[label="",style="solid", color="burlywood", weight=9];
5634 -> 4756[label="",style="solid", color="burlywood", weight=3];
5635[label="yu4390/Zero",fontsize=10,color="white",style="solid",shape="box"];4743 -> 5635[label="",style="solid", color="burlywood", weight=9];
5635 -> 4757[label="",style="solid", color="burlywood", weight=3];
4895[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Pos (primMulNat yu4530 Zero)) (Pos (Succ yu450) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="box"];5636[label="yu4530/Succ yu45300",fontsize=10,color="white",style="solid",shape="box"];4895 -> 5636[label="",style="solid", color="burlywood", weight=9];
5636 -> 4910[label="",style="solid", color="burlywood", weight=3];
5637[label="yu4530/Zero",fontsize=10,color="white",style="solid",shape="box"];4895 -> 5637[label="",style="solid", color="burlywood", weight=9];
5637 -> 4911[label="",style="solid", color="burlywood", weight=3];
4896[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Neg (primMulNat yu4530 Zero)) (Pos (Succ yu450) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="box"];5638[label="yu4530/Succ yu45300",fontsize=10,color="white",style="solid",shape="box"];4896 -> 5638[label="",style="solid", color="burlywood", weight=9];
5638 -> 4912[label="",style="solid", color="burlywood", weight=3];
5639[label="yu4530/Zero",fontsize=10,color="white",style="solid",shape="box"];4896 -> 5639[label="",style="solid", color="burlywood", weight=9];
5639 -> 4913[label="",style="solid", color="burlywood", weight=3];
109[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];109 -> 131[label="",style="solid", color="black", weight=3];
5151 -> 4878[label="",style="dashed", color="red", weight=0];
5151[label="primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100)",fontsize=16,color="magenta"];5151 -> 5172[label="",style="dashed", color="magenta", weight=3];
5152[label="yu3000",fontsize=16,color="green",shape="box"];5153[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (primCmpInt (Neg (primMulNat (Succ yu4760) Zero)) (Neg (Succ yu469) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5153 -> 5173[label="",style="solid", color="black", weight=3];
5154[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (primCmpInt (Neg (primMulNat Zero Zero)) (Neg (Succ yu469) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5154 -> 5174[label="",style="solid", color="black", weight=3];
114[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg Zero) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];114 -> 136[label="",style="solid", color="black", weight=3];
3066 -> 4497[label="",style="dashed", color="red", weight=0];
3066[label="primMinusNat (Succ (Succ yu30000)) (primDivNatS0 (Succ yu30000) (Succ yu31000) (primGEqNatS yu30000 yu31000))",fontsize=16,color="magenta"];3066 -> 4498[label="",style="dashed", color="magenta", weight=3];
3066 -> 4499[label="",style="dashed", color="magenta", weight=3];
3067[label="Succ yu31000",fontsize=16,color="green",shape="box"];3068[label="yu30000",fontsize=16,color="green",shape="box"];3065[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (primMulInt yu364 (Pos Zero)) (Pos (Succ yu220) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];5642[label="yu364/Pos yu3640",fontsize=10,color="white",style="solid",shape="box"];3065 -> 5642[label="",style="solid", color="burlywood", weight=9];
5642 -> 3525[label="",style="solid", color="burlywood", weight=3];
5643[label="yu364/Neg yu3640",fontsize=10,color="white",style="solid",shape="box"];3065 -> 5643[label="",style="solid", color="burlywood", weight=9];
5643 -> 3526[label="",style="solid", color="burlywood", weight=3];
3069 -> 4497[label="",style="dashed", color="red", weight=0];
3069[label="primMinusNat (Succ (Succ yu30000)) (primDivNatS0 (Succ yu30000) Zero True)",fontsize=16,color="magenta"];3069 -> 4500[label="",style="dashed", color="magenta", weight=3];
3069 -> 4501[label="",style="dashed", color="magenta", weight=3];
3070[label="Zero",fontsize=16,color="green",shape="box"];3071[label="yu30000",fontsize=16,color="green",shape="box"];118[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ (Succ yu31000)))) (primCmpInt (primMulInt (primMinusNat (Succ Zero) Zero) (Pos Zero)) (Pos (Succ (Succ yu31000)) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];118 -> 142[label="",style="solid", color="black", weight=3];
119[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primCmpInt (primMulInt (primMinusNat (Succ Zero) (Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero)))) (Pos Zero)) (Pos (Succ Zero) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];119 -> 143[label="",style="solid", color="black", weight=3];
120[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (Pos (Succ yu3100) * Pos (Succ Zero)) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];120 -> 144[label="",style="solid", color="black", weight=3];
5136[label="yu3100",fontsize=16,color="green",shape="box"];5137[label="yu3000",fontsize=16,color="green",shape="box"];5138[label="primPlusNat (Succ yu3000) (Succ yu4750)",fontsize=16,color="black",shape="box"];5138 -> 5157[label="",style="solid", color="black", weight=3];
5139[label="primPlusNat (Succ yu3000) Zero",fontsize=16,color="black",shape="box"];5139 -> 5158[label="",style="solid", color="black", weight=3];
5155[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (primCmpInt (Pos Zero) (Neg (Succ yu464) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];5155 -> 5175[label="",style="solid", color="black", weight=3];
5156 -> 5155[label="",style="dashed", color="red", weight=0];
5156[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (primCmpInt (Pos Zero) (Neg (Succ yu464) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="magenta"];125[label="floorFloor0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (Neg (Succ yu3100) * Pos (Succ Zero)) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];125 -> 150[label="",style="solid", color="black", weight=3];
4906[label="primDivNatS0 (Succ yu30000) (Succ yu31000) (primGEqNatS (Succ yu30000) (Succ yu31000))",fontsize=16,color="black",shape="box"];4906 -> 4926[label="",style="solid", color="black", weight=3];
4907[label="primDivNatS0 (Succ yu30000) Zero (primGEqNatS (Succ yu30000) Zero)",fontsize=16,color="black",shape="box"];4907 -> 4927[label="",style="solid", color="black", weight=3];
4908[label="primDivNatS0 Zero (Succ yu31000) (primGEqNatS Zero (Succ yu31000))",fontsize=16,color="black",shape="box"];4908 -> 4928[label="",style="solid", color="black", weight=3];
4909[label="primDivNatS0 Zero Zero (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];4909 -> 4929[label="",style="solid", color="black", weight=3];
4754[label="primMinusNat (Succ yu41400) (Succ yu43900)",fontsize=16,color="black",shape="box"];4754 -> 4771[label="",style="solid", color="black", weight=3];
4755[label="primMinusNat (Succ yu41400) Zero",fontsize=16,color="black",shape="box"];4755 -> 4772[label="",style="solid", color="black", weight=3];
4756[label="primMinusNat Zero (Succ yu43900)",fontsize=16,color="black",shape="box"];4756 -> 4773[label="",style="solid", color="black", weight=3];
4757[label="primMinusNat Zero Zero",fontsize=16,color="black",shape="box"];4757 -> 4774[label="",style="solid", color="black", weight=3];
4910[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Pos (primMulNat (Succ yu45300) Zero)) (Pos (Succ yu450) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];4910 -> 4930[label="",style="solid", color="black", weight=3];
4911[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Pos (primMulNat Zero Zero)) (Pos (Succ yu450) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];4911 -> 4931[label="",style="solid", color="black", weight=3];
4912[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Neg (primMulNat (Succ yu45300) Zero)) (Pos (Succ yu450) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];4912 -> 4932[label="",style="solid", color="black", weight=3];
4913[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Neg (primMulNat Zero Zero)) (Pos (Succ yu450) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];4913 -> 4933[label="",style="solid", color="black", weight=3];
131[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (Pos (Succ yu3100) * Pos (Succ Zero)) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];131 -> 158[label="",style="solid", color="black", weight=3];
5172[label="yu3100",fontsize=16,color="green",shape="box"];5173[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (primCmpInt (Neg Zero) (Neg (Succ yu469) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];5173 -> 5179[label="",style="solid", color="black", weight=3];
5174 -> 5173[label="",style="dashed", color="red", weight=0];
5174[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (primCmpInt (Neg Zero) (Neg (Succ yu469) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="magenta"];136[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg Zero) (primMulInt (Neg (Succ yu3100) * Pos (Succ Zero)) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];136 -> 164[label="",style="solid", color="black", weight=3];
4498 -> 5403[label="",style="dashed", color="red", weight=0];
4498[label="primDivNatS0 (Succ yu30000) (Succ yu31000) (primGEqNatS yu30000 yu31000)",fontsize=16,color="magenta"];4498 -> 5404[label="",style="dashed", color="magenta", weight=3];
4498 -> 5405[label="",style="dashed", color="magenta", weight=3];
4498 -> 5406[label="",style="dashed", color="magenta", weight=3];
4498 -> 5407[label="",style="dashed", color="magenta", weight=3];
4499[label="Succ yu30000",fontsize=16,color="green",shape="box"];4497[label="primMinusNat (Succ yu4140) yu439",fontsize=16,color="burlywood",shape="triangle"];5648[label="yu439/Succ yu4390",fontsize=10,color="white",style="solid",shape="box"];4497 -> 5648[label="",style="solid", color="burlywood", weight=9];
5648 -> 4718[label="",style="solid", color="burlywood", weight=3];
5649[label="yu439/Zero",fontsize=10,color="white",style="solid",shape="box"];4497 -> 5649[label="",style="solid", color="burlywood", weight=9];
5649 -> 4719[label="",style="solid", color="burlywood", weight=3];
3525[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (primMulInt (Pos yu3640) (Pos Zero)) (Pos (Succ yu220) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];3525 -> 3543[label="",style="solid", color="black", weight=3];
3526[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (primMulInt (Neg yu3640) (Pos Zero)) (Pos (Succ yu220) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];3526 -> 3544[label="",style="solid", color="black", weight=3];
4500[label="primDivNatS0 (Succ yu30000) Zero True",fontsize=16,color="black",shape="triangle"];4500 -> 4720[label="",style="solid", color="black", weight=3];
4501[label="Succ yu30000",fontsize=16,color="green",shape="box"];142[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ (Succ yu31000)))) (primCmpInt (primMulInt (Pos (Succ Zero)) (Pos Zero)) (Pos (Succ (Succ yu31000)) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];142 -> 170[label="",style="solid", color="black", weight=3];
143[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primCmpInt (primMulInt (primMinusNat Zero (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))) (Pos Zero)) (Pos (Succ Zero) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];143 -> 171[label="",style="solid", color="black", weight=3];
144[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (primMulInt (Pos (Succ yu3100)) (Pos (Succ Zero))) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];144 -> 172[label="",style="solid", color="black", weight=3];
5157[label="Succ (Succ (primPlusNat yu3000 yu4750))",fontsize=16,color="green",shape="box"];5157 -> 5176[label="",style="dashed", color="green", weight=3];
5158[label="Succ yu3000",fontsize=16,color="green",shape="box"];5175[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (primCmpInt (Pos Zero) (primMulInt (Neg (Succ yu464) * Pos (Succ Zero)) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5175 -> 5180[label="",style="solid", color="black", weight=3];
150[label="floorFloor0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (primMulInt (Neg (Succ yu3100)) (Pos (Succ Zero))) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];150 -> 180[label="",style="solid", color="black", weight=3];
4926 -> 5403[label="",style="dashed", color="red", weight=0];
4926[label="primDivNatS0 (Succ yu30000) (Succ yu31000) (primGEqNatS yu30000 yu31000)",fontsize=16,color="magenta"];4926 -> 5408[label="",style="dashed", color="magenta", weight=3];
4926 -> 5409[label="",style="dashed", color="magenta", weight=3];
4926 -> 5410[label="",style="dashed", color="magenta", weight=3];
4926 -> 5411[label="",style="dashed", color="magenta", weight=3];
4927 -> 4500[label="",style="dashed", color="red", weight=0];
4927[label="primDivNatS0 (Succ yu30000) Zero True",fontsize=16,color="magenta"];4927 -> 4945[label="",style="dashed", color="magenta", weight=3];
4928[label="primDivNatS0 Zero (Succ yu31000) False",fontsize=16,color="black",shape="box"];4928 -> 4946[label="",style="solid", color="black", weight=3];
4929 -> 3689[label="",style="dashed", color="red", weight=0];
4929[label="primDivNatS0 Zero Zero True",fontsize=16,color="magenta"];4771 -> 4730[label="",style="dashed", color="red", weight=0];
4771[label="primMinusNat yu41400 yu43900",fontsize=16,color="magenta"];4771 -> 4786[label="",style="dashed", color="magenta", weight=3];
4771 -> 4787[label="",style="dashed", color="magenta", weight=3];
4772[label="Pos (Succ yu41400)",fontsize=16,color="green",shape="box"];4773[label="Neg (Succ yu43900)",fontsize=16,color="green",shape="box"];4774[label="Pos Zero",fontsize=16,color="green",shape="box"];4930[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Pos Zero) (Pos (Succ yu450) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];4930 -> 4947[label="",style="solid", color="black", weight=3];
4931 -> 4930[label="",style="dashed", color="red", weight=0];
4931[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Pos Zero) (Pos (Succ yu450) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="magenta"];4932[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Neg Zero) (Pos (Succ yu450) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];4932 -> 4948[label="",style="solid", color="black", weight=3];
4933 -> 4932[label="",style="dashed", color="red", weight=0];
4933[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Neg Zero) (Pos (Succ yu450) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="magenta"];158[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (primMulInt (Pos (Succ yu3100)) (Pos (Succ Zero))) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];158 -> 188[label="",style="solid", color="black", weight=3];
5179[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (primCmpInt (Neg Zero) (primMulInt (Neg (Succ yu469) * Pos (Succ Zero)) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5179 -> 5185[label="",style="solid", color="black", weight=3];
164[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg Zero) (primMulInt (primMulInt (Neg (Succ yu3100)) (Pos (Succ Zero))) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];164 -> 196[label="",style="solid", color="black", weight=3];
5404[label="yu30000",fontsize=16,color="green",shape="box"];5405[label="yu31000",fontsize=16,color="green",shape="box"];5406[label="yu30000",fontsize=16,color="green",shape="box"];5407[label="yu31000",fontsize=16,color="green",shape="box"];5403[label="primDivNatS0 (Succ yu497) (Succ yu498) (primGEqNatS yu499 yu500)",fontsize=16,color="burlywood",shape="triangle"];5656[label="yu499/Succ yu4990",fontsize=10,color="white",style="solid",shape="box"];5403 -> 5656[label="",style="solid", color="burlywood", weight=9];
5656 -> 5448[label="",style="solid", color="burlywood", weight=3];
5657[label="yu499/Zero",fontsize=10,color="white",style="solid",shape="box"];5403 -> 5657[label="",style="solid", color="burlywood", weight=9];
5657 -> 5449[label="",style="solid", color="burlywood", weight=3];
4718[label="primMinusNat (Succ yu4140) (Succ yu4390)",fontsize=16,color="black",shape="box"];4718 -> 4730[label="",style="solid", color="black", weight=3];
4719[label="primMinusNat (Succ yu4140) Zero",fontsize=16,color="black",shape="box"];4719 -> 4731[label="",style="solid", color="black", weight=3];
3543[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Pos (primMulNat yu3640 Zero)) (Pos (Succ yu220) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="box"];5658[label="yu3640/Succ yu36400",fontsize=10,color="white",style="solid",shape="box"];3543 -> 5658[label="",style="solid", color="burlywood", weight=9];
5658 -> 3552[label="",style="solid", color="burlywood", weight=3];
5659[label="yu3640/Zero",fontsize=10,color="white",style="solid",shape="box"];3543 -> 5659[label="",style="solid", color="burlywood", weight=9];
5659 -> 3553[label="",style="solid", color="burlywood", weight=3];
3544[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Neg (primMulNat yu3640 Zero)) (Pos (Succ yu220) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="box"];5660[label="yu3640/Succ yu36400",fontsize=10,color="white",style="solid",shape="box"];3544 -> 5660[label="",style="solid", color="burlywood", weight=9];
5660 -> 3554[label="",style="solid", color="burlywood", weight=3];
5661[label="yu3640/Zero",fontsize=10,color="white",style="solid",shape="box"];3544 -> 5661[label="",style="solid", color="burlywood", weight=9];
5661 -> 3555[label="",style="solid", color="burlywood", weight=3];
4720[label="Succ (primDivNatS (primMinusNatS (Succ yu30000) Zero) (Succ Zero))",fontsize=16,color="green",shape="box"];4720 -> 4732[label="",style="dashed", color="green", weight=3];
170[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ (Succ yu31000)))) (primCmpInt (Pos (primMulNat (Succ Zero) Zero)) (Pos (Succ (Succ yu31000)) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];170 -> 203[label="",style="solid", color="black", weight=3];
171[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primCmpInt (primMulInt (primMinusNat Zero (primDivNatS Zero (Succ Zero))) (Pos Zero)) (Pos (Succ Zero) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];171 -> 204[label="",style="solid", color="black", weight=3];
172[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (Pos (primMulNat (Succ yu3100) (Succ Zero))) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];172 -> 205[label="",style="solid", color="black", weight=3];
5176[label="primPlusNat yu3000 yu4750",fontsize=16,color="burlywood",shape="triangle"];5662[label="yu3000/Succ yu30000",fontsize=10,color="white",style="solid",shape="box"];5176 -> 5662[label="",style="solid", color="burlywood", weight=9];
5662 -> 5181[label="",style="solid", color="burlywood", weight=3];
5663[label="yu3000/Zero",fontsize=10,color="white",style="solid",shape="box"];5176 -> 5663[label="",style="solid", color="burlywood", weight=9];
5663 -> 5182[label="",style="solid", color="burlywood", weight=3];
5180[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (primCmpInt (Pos Zero) (primMulInt (primMulInt (Neg (Succ yu464)) (Pos (Succ Zero))) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5180 -> 5186[label="",style="solid", color="black", weight=3];
180[label="floorFloor0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (Neg (primMulNat (Succ yu3100) (Succ Zero))) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];180 -> 213[label="",style="solid", color="black", weight=3];
5408[label="yu30000",fontsize=16,color="green",shape="box"];5409[label="yu31000",fontsize=16,color="green",shape="box"];5410[label="yu30000",fontsize=16,color="green",shape="box"];5411[label="yu31000",fontsize=16,color="green",shape="box"];4945[label="yu30000",fontsize=16,color="green",shape="box"];4946[label="Zero",fontsize=16,color="green",shape="box"];3689[label="primDivNatS0 Zero Zero True",fontsize=16,color="black",shape="triangle"];3689 -> 3705[label="",style="solid", color="black", weight=3];
4786[label="yu41400",fontsize=16,color="green",shape="box"];4787[label="yu43900",fontsize=16,color="green",shape="box"];4947[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Pos Zero) (primMulInt (Pos (Succ yu450) * Pos (Succ Zero)) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];4947 -> 5024[label="",style="solid", color="black", weight=3];
4948[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Neg Zero) (primMulInt (Pos (Succ yu450) * Pos (Succ Zero)) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];4948 -> 5025[label="",style="solid", color="black", weight=3];
188[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (Pos (primMulNat (Succ yu3100) (Succ Zero))) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];188 -> 222[label="",style="solid", color="black", weight=3];
5185[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (primCmpInt (Neg Zero) (primMulInt (primMulInt (Neg (Succ yu469)) (Pos (Succ Zero))) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5185 -> 5202[label="",style="solid", color="black", weight=3];
196[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg Zero) (primMulInt (Neg (primMulNat (Succ yu3100) (Succ Zero))) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];196 -> 230[label="",style="solid", color="black", weight=3];
5448[label="primDivNatS0 (Succ yu497) (Succ yu498) (primGEqNatS (Succ yu4990) yu500)",fontsize=16,color="burlywood",shape="box"];5664[label="yu500/Succ yu5000",fontsize=10,color="white",style="solid",shape="box"];5448 -> 5664[label="",style="solid", color="burlywood", weight=9];
5664 -> 5455[label="",style="solid", color="burlywood", weight=3];
5665[label="yu500/Zero",fontsize=10,color="white",style="solid",shape="box"];5448 -> 5665[label="",style="solid", color="burlywood", weight=9];
5665 -> 5456[label="",style="solid", color="burlywood", weight=3];
5449[label="primDivNatS0 (Succ yu497) (Succ yu498) (primGEqNatS Zero yu500)",fontsize=16,color="burlywood",shape="box"];5666[label="yu500/Succ yu5000",fontsize=10,color="white",style="solid",shape="box"];5449 -> 5666[label="",style="solid", color="burlywood", weight=9];
5666 -> 5457[label="",style="solid", color="burlywood", weight=3];
5667[label="yu500/Zero",fontsize=10,color="white",style="solid",shape="box"];5449 -> 5667[label="",style="solid", color="burlywood", weight=9];
5667 -> 5458[label="",style="solid", color="burlywood", weight=3];
4731[label="Pos (Succ yu4140)",fontsize=16,color="green",shape="box"];3552[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Pos (primMulNat (Succ yu36400) Zero)) (Pos (Succ yu220) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];3552 -> 3589[label="",style="solid", color="black", weight=3];
3553[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Pos (primMulNat Zero Zero)) (Pos (Succ yu220) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];3553 -> 3590[label="",style="solid", color="black", weight=3];
3554[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Neg (primMulNat (Succ yu36400) Zero)) (Pos (Succ yu220) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];3554 -> 3591[label="",style="solid", color="black", weight=3];
3555[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Neg (primMulNat Zero Zero)) (Pos (Succ yu220) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];3555 -> 3592[label="",style="solid", color="black", weight=3];
4732 -> 5537[label="",style="dashed", color="red", weight=0];
4732[label="primDivNatS (primMinusNatS (Succ yu30000) Zero) (Succ Zero)",fontsize=16,color="magenta"];4732 -> 5538[label="",style="dashed", color="magenta", weight=3];
4732 -> 5539[label="",style="dashed", color="magenta", weight=3];
4732 -> 5540[label="",style="dashed", color="magenta", weight=3];
203[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ (Succ yu31000)))) (primCmpInt (Pos Zero) (Pos (Succ (Succ yu31000)) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];203 -> 240[label="",style="solid", color="black", weight=3];
204[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primCmpInt (primMulInt (primMinusNat Zero Zero) (Pos Zero)) (Pos (Succ Zero) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];204 -> 241[label="",style="solid", color="black", weight=3];
205 -> 1460[label="",style="dashed", color="red", weight=0];
205[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (Pos (primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero))) == LT)",fontsize=16,color="magenta"];205 -> 1461[label="",style="dashed", color="magenta", weight=3];
205 -> 1462[label="",style="dashed", color="magenta", weight=3];
5181[label="primPlusNat (Succ yu30000) yu4750",fontsize=16,color="burlywood",shape="box"];5670[label="yu4750/Succ yu47500",fontsize=10,color="white",style="solid",shape="box"];5181 -> 5670[label="",style="solid", color="burlywood", weight=9];
5670 -> 5187[label="",style="solid", color="burlywood", weight=3];
5671[label="yu4750/Zero",fontsize=10,color="white",style="solid",shape="box"];5181 -> 5671[label="",style="solid", color="burlywood", weight=9];
5671 -> 5188[label="",style="solid", color="burlywood", weight=3];
5182[label="primPlusNat Zero yu4750",fontsize=16,color="burlywood",shape="box"];5672[label="yu4750/Succ yu47500",fontsize=10,color="white",style="solid",shape="box"];5182 -> 5672[label="",style="solid", color="burlywood", weight=9];
5672 -> 5189[label="",style="solid", color="burlywood", weight=3];
5673[label="yu4750/Zero",fontsize=10,color="white",style="solid",shape="box"];5182 -> 5673[label="",style="solid", color="burlywood", weight=9];
5673 -> 5190[label="",style="solid", color="burlywood", weight=3];
5186 -> 5203[label="",style="dashed", color="red", weight=0];
5186[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (primCmpInt (Pos Zero) (primMulInt (Neg (primMulNat (Succ yu464) (Succ Zero))) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="magenta"];5186 -> 5204[label="",style="dashed", color="magenta", weight=3];
213 -> 1642[label="",style="dashed", color="red", weight=0];
213[label="floorFloor0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos Zero) (Neg (primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero))) == LT)",fontsize=16,color="magenta"];213 -> 1643[label="",style="dashed", color="magenta", weight=3];
213 -> 1644[label="",style="dashed", color="magenta", weight=3];
3705[label="Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))",fontsize=16,color="green",shape="box"];3705 -> 3733[label="",style="dashed", color="green", weight=3];
5024[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Pos Zero) (primMulInt (primMulInt (Pos (Succ yu450)) (Pos (Succ Zero))) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5024 -> 5082[label="",style="solid", color="black", weight=3];
5025[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Neg Zero) (primMulInt (primMulInt (Pos (Succ yu450)) (Pos (Succ Zero))) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5025 -> 5083[label="",style="solid", color="black", weight=3];
222 -> 1829[label="",style="dashed", color="red", weight=0];
222[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (Pos (primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero))) == LT)",fontsize=16,color="magenta"];222 -> 1830[label="",style="dashed", color="magenta", weight=3];
222 -> 1831[label="",style="dashed", color="magenta", weight=3];
5202 -> 5205[label="",style="dashed", color="red", weight=0];
5202[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (primCmpInt (Neg Zero) (primMulInt (Neg (primMulNat (Succ yu469) (Succ Zero))) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="magenta"];5202 -> 5206[label="",style="dashed", color="magenta", weight=3];
230 -> 2054[label="",style="dashed", color="red", weight=0];
230[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg Zero) (Neg (primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero))) == LT)",fontsize=16,color="magenta"];230 -> 2055[label="",style="dashed", color="magenta", weight=3];
230 -> 2056[label="",style="dashed", color="magenta", weight=3];
5455[label="primDivNatS0 (Succ yu497) (Succ yu498) (primGEqNatS (Succ yu4990) (Succ yu5000))",fontsize=16,color="black",shape="box"];5455 -> 5464[label="",style="solid", color="black", weight=3];
5456[label="primDivNatS0 (Succ yu497) (Succ yu498) (primGEqNatS (Succ yu4990) Zero)",fontsize=16,color="black",shape="box"];5456 -> 5465[label="",style="solid", color="black", weight=3];
5457[label="primDivNatS0 (Succ yu497) (Succ yu498) (primGEqNatS Zero (Succ yu5000))",fontsize=16,color="black",shape="box"];5457 -> 5466[label="",style="solid", color="black", weight=3];
5458[label="primDivNatS0 (Succ yu497) (Succ yu498) (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];5458 -> 5467[label="",style="solid", color="black", weight=3];
3589[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Pos Zero) (Pos (Succ yu220) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];3589 -> 3629[label="",style="solid", color="black", weight=3];
3590 -> 3589[label="",style="dashed", color="red", weight=0];
3590[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Pos Zero) (Pos (Succ yu220) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="magenta"];3591[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Neg Zero) (Pos (Succ yu220) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];3591 -> 3630[label="",style="solid", color="black", weight=3];
3592 -> 3591[label="",style="dashed", color="red", weight=0];
3592[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Neg Zero) (Pos (Succ yu220) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)\n  Integral a",fontsize=16,color="magenta"];5538[label="Succ yu30000",fontsize=16,color="green",shape="box"];5539[label="Zero",fontsize=16,color="green",shape="box"];5540[label="Zero",fontsize=16,color="green",shape="box"];5537[label="primDivNatS (primMinusNatS yu502 yu503) (Succ yu504)",fontsize=16,color="burlywood",shape="triangle"];5681[label="yu502/Succ yu5020",fontsize=10,color="white",style="solid",shape="box"];5537 -> 5681[label="",style="solid", color="burlywood", weight=9];
5681 -> 5562[label="",style="solid", color="burlywood", weight=3];
5682[label="yu502/Zero",fontsize=10,color="white",style="solid",shape="box"];5537 -> 5682[label="",style="solid", color="burlywood", weight=9];
5682 -> 5563[label="",style="solid", color="burlywood", weight=3];
240[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ (Succ yu31000)))) (primCmpInt (Pos Zero) (primMulInt (Pos (Succ (Succ yu31000)) * Pos (Succ Zero)) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];240 -> 282[label="",style="solid", color="black", weight=3];
241[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primCmpInt (primMulInt (Pos Zero) (Pos Zero)) (Pos (Succ Zero) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];241 -> 283[label="",style="solid", color="black", weight=3];
1461 -> 1571[label="",style="dashed", color="red", weight=0];
1461[label="primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];1461 -> 1572[label="",style="dashed", color="magenta", weight=3];
1462[label="yu3100",fontsize=16,color="green",shape="box"];1460[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu71))) (primCmpInt (Pos Zero) (Pos yu102) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];5684[label="yu102/Succ yu1020",fontsize=10,color="white",style="solid",shape="box"];1460 -> 5684[label="",style="solid", color="burlywood", weight=9];
5684 -> 1479[label="",style="solid", color="burlywood", weight=3];
5685[label="yu102/Zero",fontsize=10,color="white",style="solid",shape="box"];1460 -> 5685[label="",style="solid", color="burlywood", weight=9];
5685 -> 1480[label="",style="solid", color="burlywood", weight=3];
5187[label="primPlusNat (Succ yu30000) (Succ yu47500)",fontsize=16,color="black",shape="box"];5187 -> 5207[label="",style="solid", color="black", weight=3];
5188[label="primPlusNat (Succ yu30000) Zero",fontsize=16,color="black",shape="box"];5188 -> 5208[label="",style="solid", color="black", weight=3];
5189[label="primPlusNat Zero (Succ yu47500)",fontsize=16,color="black",shape="box"];5189 -> 5209[label="",style="solid", color="black", weight=3];
5190[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];5190 -> 5210[label="",style="solid", color="black", weight=3];
5204 -> 1571[label="",style="dashed", color="red", weight=0];
5204[label="primMulNat (Succ yu464) (Succ Zero)",fontsize=16,color="magenta"];5204 -> 5211[label="",style="dashed", color="magenta", weight=3];
5203[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (primCmpInt (Pos Zero) (primMulInt (Neg yu481) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];5203 -> 5212[label="",style="solid", color="black", weight=3];
1643[label="yu3100",fontsize=16,color="green",shape="box"];1644 -> 1571[label="",style="dashed", color="red", weight=0];
1644[label="primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];1644 -> 1710[label="",style="dashed", color="magenta", weight=3];
1642[label="floorFloor0 (Float (Pos Zero) (Neg (Succ yu78))) (primCmpInt (Pos Zero) (Neg yu120) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];5688[label="yu120/Succ yu1200",fontsize=10,color="white",style="solid",shape="box"];1642 -> 5688[label="",style="solid", color="burlywood", weight=9];
5688 -> 1711[label="",style="solid", color="burlywood", weight=3];
5689[label="yu120/Zero",fontsize=10,color="white",style="solid",shape="box"];1642 -> 5689[label="",style="solid", color="burlywood", weight=9];
5689 -> 1712[label="",style="solid", color="burlywood", weight=3];
3733 -> 5537[label="",style="dashed", color="red", weight=0];
3733[label="primDivNatS (primMinusNatS Zero Zero) (Succ Zero)",fontsize=16,color="magenta"];3733 -> 5541[label="",style="dashed", color="magenta", weight=3];
3733 -> 5542[label="",style="dashed", color="magenta", weight=3];
3733 -> 5543[label="",style="dashed", color="magenta", weight=3];
5082 -> 5103[label="",style="dashed", color="red", weight=0];
5082[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Pos Zero) (primMulInt (Pos (primMulNat (Succ yu450) (Succ Zero))) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="magenta"];5082 -> 5104[label="",style="dashed", color="magenta", weight=3];
5083 -> 5113[label="",style="dashed", color="red", weight=0];
5083[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Neg Zero) (primMulInt (Pos (primMulNat (Succ yu450) (Succ Zero))) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="magenta"];5083 -> 5114[label="",style="dashed", color="magenta", weight=3];
1830[label="yu3100",fontsize=16,color="green",shape="box"];1831 -> 1571[label="",style="dashed", color="red", weight=0];
1831[label="primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];1831 -> 1897[label="",style="dashed", color="magenta", weight=3];
1829[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu87))) (primCmpInt (Pos Zero) (Pos yu162) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];5694[label="yu162/Succ yu1620",fontsize=10,color="white",style="solid",shape="box"];1829 -> 5694[label="",style="solid", color="burlywood", weight=9];
5694 -> 1898[label="",style="solid", color="burlywood", weight=3];
5695[label="yu162/Zero",fontsize=10,color="white",style="solid",shape="box"];1829 -> 5695[label="",style="solid", color="burlywood", weight=9];
5695 -> 1899[label="",style="solid", color="burlywood", weight=3];
5206 -> 1571[label="",style="dashed", color="red", weight=0];
5206[label="primMulNat (Succ yu469) (Succ Zero)",fontsize=16,color="magenta"];5206 -> 5213[label="",style="dashed", color="magenta", weight=3];
5205[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (primCmpInt (Neg Zero) (primMulInt (Neg yu482) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];5205 -> 5214[label="",style="solid", color="black", weight=3];
2055[label="yu3100",fontsize=16,color="green",shape="box"];2056 -> 1571[label="",style="dashed", color="red", weight=0];
2056[label="primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];2056 -> 2122[label="",style="dashed", color="magenta", weight=3];
2054[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu94))) (primCmpInt (Neg Zero) (Neg yu210) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];5698[label="yu210/Succ yu2100",fontsize=10,color="white",style="solid",shape="box"];2054 -> 5698[label="",style="solid", color="burlywood", weight=9];
5698 -> 2123[label="",style="solid", color="burlywood", weight=3];
5699[label="yu210/Zero",fontsize=10,color="white",style="solid",shape="box"];2054 -> 5699[label="",style="solid", color="burlywood", weight=9];
5699 -> 2124[label="",style="solid", color="burlywood", weight=3];
5464 -> 5403[label="",style="dashed", color="red", weight=0];
5464[label="primDivNatS0 (Succ yu497) (Succ yu498) (primGEqNatS yu4990 yu5000)",fontsize=16,color="magenta"];5464 -> 5471[label="",style="dashed", color="magenta", weight=3];
5464 -> 5472[label="",style="dashed", color="magenta", weight=3];
5465[label="primDivNatS0 (Succ yu497) (Succ yu498) True",fontsize=16,color="black",shape="triangle"];5465 -> 5473[label="",style="solid", color="black", weight=3];
5466[label="primDivNatS0 (Succ yu497) (Succ yu498) False",fontsize=16,color="black",shape="box"];5466 -> 5474[label="",style="solid", color="black", weight=3];
5467 -> 5465[label="",style="dashed", color="red", weight=0];
5467[label="primDivNatS0 (Succ yu497) (Succ yu498) True",fontsize=16,color="magenta"];3629[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Pos Zero) (primMulInt (Pos (Succ yu220) * Pos (Succ Zero)) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];3629 -> 3654[label="",style="solid", color="black", weight=3];
3630[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Neg Zero) (primMulInt (Pos (Succ yu220) * Pos (Succ Zero)) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];3630 -> 3655[label="",style="solid", color="black", weight=3];
5562[label="primDivNatS (primMinusNatS (Succ yu5020) yu503) (Succ yu504)",fontsize=16,color="burlywood",shape="box"];5702[label="yu503/Succ yu5030",fontsize=10,color="white",style="solid",shape="box"];5562 -> 5702[label="",style="solid", color="burlywood", weight=9];
5702 -> 5564[label="",style="solid", color="burlywood", weight=3];
5703[label="yu503/Zero",fontsize=10,color="white",style="solid",shape="box"];5562 -> 5703[label="",style="solid", color="burlywood", weight=9];
5703 -> 5565[label="",style="solid", color="burlywood", weight=3];
5563[label="primDivNatS (primMinusNatS Zero yu503) (Succ yu504)",fontsize=16,color="burlywood",shape="box"];5704[label="yu503/Succ yu5030",fontsize=10,color="white",style="solid",shape="box"];5563 -> 5704[label="",style="solid", color="burlywood", weight=9];
5704 -> 5566[label="",style="solid", color="burlywood", weight=3];
5705[label="yu503/Zero",fontsize=10,color="white",style="solid",shape="box"];5563 -> 5705[label="",style="solid", color="burlywood", weight=9];
5705 -> 5567[label="",style="solid", color="burlywood", weight=3];
282[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ (Succ yu31000)))) (primCmpInt (Pos Zero) (primMulInt (primMulInt (Pos (Succ (Succ yu31000))) (Pos (Succ Zero))) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];282 -> 333[label="",style="solid", color="black", weight=3];
283[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primCmpInt (Pos (primMulNat Zero Zero)) (Pos (Succ Zero) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];283 -> 334[label="",style="solid", color="black", weight=3];
1572 -> 1571[label="",style="dashed", color="red", weight=0];
1572[label="primMulNat (Succ yu3100) (Succ Zero)",fontsize=16,color="magenta"];1572 -> 1587[label="",style="dashed", color="magenta", weight=3];
1571[label="primMulNat yu112 (Succ Zero)",fontsize=16,color="burlywood",shape="triangle"];5707[label="yu112/Succ yu1120",fontsize=10,color="white",style="solid",shape="box"];1571 -> 5707[label="",style="solid", color="burlywood", weight=9];
5707 -> 1588[label="",style="solid", color="burlywood", weight=3];
5708[label="yu112/Zero",fontsize=10,color="white",style="solid",shape="box"];1571 -> 5708[label="",style="solid", color="burlywood", weight=9];
5708 -> 1589[label="",style="solid", color="burlywood", weight=3];
1479[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu71))) (primCmpInt (Pos Zero) (Pos (Succ yu1020)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];1479 -> 1485[label="",style="solid", color="black", weight=3];
1480[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu71))) (primCmpInt (Pos Zero) (Pos Zero) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];1480 -> 1486[label="",style="solid", color="black", weight=3];
5207[label="Succ (Succ (primPlusNat yu30000 yu47500))",fontsize=16,color="green",shape="box"];5207 -> 5256[label="",style="dashed", color="green", weight=3];
5208[label="Succ yu30000",fontsize=16,color="green",shape="box"];5209[label="Succ yu47500",fontsize=16,color="green",shape="box"];5210[label="Zero",fontsize=16,color="green",shape="box"];5211[label="Succ yu464",fontsize=16,color="green",shape="box"];5212 -> 5257[label="",style="dashed", color="red", weight=0];
5212[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (primCmpInt (Pos Zero) (Neg (primMulNat yu481 (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="magenta"];5212 -> 5258[label="",style="dashed", color="magenta", weight=3];
1710 -> 1571[label="",style="dashed", color="red", weight=0];
1710[label="primMulNat (Succ yu3100) (Succ Zero)",fontsize=16,color="magenta"];1710 -> 1733[label="",style="dashed", color="magenta", weight=3];
1711[label="floorFloor0 (Float (Pos Zero) (Neg (Succ yu78))) (primCmpInt (Pos Zero) (Neg (Succ yu1200)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];1711 -> 1734[label="",style="solid", color="black", weight=3];
1712[label="floorFloor0 (Float (Pos Zero) (Neg (Succ yu78))) (primCmpInt (Pos Zero) (Neg Zero) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];1712 -> 1735[label="",style="solid", color="black", weight=3];
5541[label="Zero",fontsize=16,color="green",shape="box"];5542[label="Zero",fontsize=16,color="green",shape="box"];5543[label="Zero",fontsize=16,color="green",shape="box"];5104 -> 1571[label="",style="dashed", color="red", weight=0];
5104[label="primMulNat (Succ yu450) (Succ Zero)",fontsize=16,color="magenta"];5104 -> 5159[label="",style="dashed", color="magenta", weight=3];
5103[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Pos Zero) (primMulInt (Pos yu472) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];5103 -> 5160[label="",style="solid", color="black", weight=3];
5114 -> 1571[label="",style="dashed", color="red", weight=0];
5114[label="primMulNat (Succ yu450) (Succ Zero)",fontsize=16,color="magenta"];5114 -> 5161[label="",style="dashed", color="magenta", weight=3];
5113[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Neg Zero) (primMulInt (Pos yu473) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];5113 -> 5162[label="",style="solid", color="black", weight=3];
1897 -> 1571[label="",style="dashed", color="red", weight=0];
1897[label="primMulNat (Succ yu3100) (Succ Zero)",fontsize=16,color="magenta"];1897 -> 1916[label="",style="dashed", color="magenta", weight=3];
1898[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu87))) (primCmpInt (Pos Zero) (Pos (Succ yu1620)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];1898 -> 1917[label="",style="solid", color="black", weight=3];
1899[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu87))) (primCmpInt (Pos Zero) (Pos Zero) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];1899 -> 1918[label="",style="solid", color="black", weight=3];
5213[label="Succ yu469",fontsize=16,color="green",shape="box"];5214 -> 5259[label="",style="dashed", color="red", weight=0];
5214[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (primCmpInt (Neg Zero) (Neg (primMulNat yu482 (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="magenta"];5214 -> 5260[label="",style="dashed", color="magenta", weight=3];
2122 -> 1571[label="",style="dashed", color="red", weight=0];
2122[label="primMulNat (Succ yu3100) (Succ Zero)",fontsize=16,color="magenta"];2122 -> 2144[label="",style="dashed", color="magenta", weight=3];
2123[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu94))) (primCmpInt (Neg Zero) (Neg (Succ yu2100)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];2123 -> 2145[label="",style="solid", color="black", weight=3];
2124[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu94))) (primCmpInt (Neg Zero) (Neg Zero) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];2124 -> 2146[label="",style="solid", color="black", weight=3];
5471[label="yu4990",fontsize=16,color="green",shape="box"];5472[label="yu5000",fontsize=16,color="green",shape="box"];5473[label="Succ (primDivNatS (primMinusNatS (Succ yu497) (Succ yu498)) (Succ (Succ yu498)))",fontsize=16,color="green",shape="box"];5473 -> 5479[label="",style="dashed", color="green", weight=3];
5474[label="Zero",fontsize=16,color="green",shape="box"];3654[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Pos Zero) (primMulInt (primMulInt (Pos (Succ yu220)) (Pos (Succ Zero))) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];3654 -> 3686[label="",style="solid", color="black", weight=3];
3655[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Neg Zero) (primMulInt (primMulInt (Pos (Succ yu220)) (Pos (Succ Zero))) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];3655 -> 3687[label="",style="solid", color="black", weight=3];
5564[label="primDivNatS (primMinusNatS (Succ yu5020) (Succ yu5030)) (Succ yu504)",fontsize=16,color="black",shape="box"];5564 -> 5568[label="",style="solid", color="black", weight=3];
5565[label="primDivNatS (primMinusNatS (Succ yu5020) Zero) (Succ yu504)",fontsize=16,color="black",shape="box"];5565 -> 5569[label="",style="solid", color="black", weight=3];
5566[label="primDivNatS (primMinusNatS Zero (Succ yu5030)) (Succ yu504)",fontsize=16,color="black",shape="box"];5566 -> 5570[label="",style="solid", color="black", weight=3];
5567[label="primDivNatS (primMinusNatS Zero Zero) (Succ yu504)",fontsize=16,color="black",shape="box"];5567 -> 5571[label="",style="solid", color="black", weight=3];
333[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ (Succ yu31000)))) (primCmpInt (Pos Zero) (primMulInt (Pos (primMulNat (Succ (Succ yu31000)) (Succ Zero))) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];333 -> 391[label="",style="solid", color="black", weight=3];
334[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primCmpInt (Pos Zero) (Pos (Succ Zero) * Pos (Succ Zero) * Pos (Succ Zero)) == LT)",fontsize=16,color="black",shape="box"];334 -> 392[label="",style="solid", color="black", weight=3];
1587[label="Succ yu3100",fontsize=16,color="green",shape="box"];1588[label="primMulNat (Succ yu1120) (Succ Zero)",fontsize=16,color="black",shape="box"];1588 -> 1592[label="",style="solid", color="black", weight=3];
1589[label="primMulNat Zero (Succ Zero)",fontsize=16,color="black",shape="box"];1589 -> 1593[label="",style="solid", color="black", weight=3];
1485[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu71))) (primCmpNat Zero (Succ yu1020) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];1485 -> 1500[label="",style="solid", color="black", weight=3];
1486[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu71))) (EQ == LT)\n  Integral a",fontsize=16,color="black",shape="box"];1486 -> 1501[label="",style="solid", color="black", weight=3];
5256 -> 5176[label="",style="dashed", color="red", weight=0];
5256[label="primPlusNat yu30000 yu47500",fontsize=16,color="magenta"];5256 -> 5262[label="",style="dashed", color="magenta", weight=3];
5256 -> 5263[label="",style="dashed", color="magenta", weight=3];
5258 -> 1571[label="",style="dashed", color="red", weight=0];
5258[label="primMulNat yu481 (Succ Zero)",fontsize=16,color="magenta"];5258 -> 5264[label="",style="dashed", color="magenta", weight=3];
5257[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (primCmpInt (Pos Zero) (Neg yu486) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];5718[label="yu486/Succ yu4860",fontsize=10,color="white",style="solid",shape="box"];5257 -> 5718[label="",style="solid", color="burlywood", weight=9];
5718 -> 5265[label="",style="solid", color="burlywood", weight=3];
5719[label="yu486/Zero",fontsize=10,color="white",style="solid",shape="box"];5257 -> 5719[label="",style="solid", color="burlywood", weight=9];
5719 -> 5266[label="",style="solid", color="burlywood", weight=3];
1733[label="Succ yu3100",fontsize=16,color="green",shape="box"];1734[label="floorFloor0 (Float (Pos Zero) (Neg (Succ yu78))) (GT == LT)\n  Integral a",fontsize=16,color="black",shape="box"];1734 -> 1753[label="",style="solid", color="black", weight=3];
1735[label="floorFloor0 (Float (Pos Zero) (Neg (Succ yu78))) (EQ == LT)\n  Integral a",fontsize=16,color="black",shape="box"];1735 -> 1754[label="",style="solid", color="black", weight=3];
5159[label="Succ yu450",fontsize=16,color="green",shape="box"];5160 -> 5177[label="",style="dashed", color="red", weight=0];
5160[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Pos Zero) (Pos (primMulNat yu472 (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="magenta"];5160 -> 5178[label="",style="dashed", color="magenta", weight=3];
5161[label="Succ yu450",fontsize=16,color="green",shape="box"];5162 -> 5183[label="",style="dashed", color="red", weight=0];
5162[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Neg Zero) (Pos (primMulNat yu473 (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="magenta"];5162 -> 5184[label="",style="dashed", color="magenta", weight=3];
1916[label="Succ yu3100",fontsize=16,color="green",shape="box"];1917[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu87))) (primCmpNat Zero (Succ yu1620) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];1917 -> 1930[label="",style="solid", color="black", weight=3];
1918[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu87))) (EQ == LT)\n  Integral a",fontsize=16,color="black",shape="box"];1918 -> 1931[label="",style="solid", color="black", weight=3];
5260 -> 1571[label="",style="dashed", color="red", weight=0];
5260[label="primMulNat yu482 (Succ Zero)",fontsize=16,color="magenta"];5260 -> 5267[label="",style="dashed", color="magenta", weight=3];
5259[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (primCmpInt (Neg Zero) (Neg yu487) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];5723[label="yu487/Succ yu4870",fontsize=10,color="white",style="solid",shape="box"];5259 -> 5723[label="",style="solid", color="burlywood", weight=9];
5723 -> 5268[label="",style="solid", color="burlywood", weight=3];
5724[label="yu487/Zero",fontsize=10,color="white",style="solid",shape="box"];5259 -> 5724[label="",style="solid", color="burlywood", weight=9];
5724 -> 5269[label="",style="solid", color="burlywood", weight=3];
2144[label="Succ yu3100",fontsize=16,color="green",shape="box"];2145[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu94))) (primCmpNat (Succ yu2100) Zero == LT)\n  Integral a",fontsize=16,color="black",shape="box"];2145 -> 2156[label="",style="solid", color="black", weight=3];
2146[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu94))) (EQ == LT)\n  Integral a",fontsize=16,color="black",shape="box"];2146 -> 2157[label="",style="solid", color="black", weight=3];
5479 -> 5537[label="",style="dashed", color="red", weight=0];
5479[label="primDivNatS (primMinusNatS (Succ yu497) (Succ yu498)) (Succ (Succ yu498))",fontsize=16,color="magenta"];5479 -> 5544[label="",style="dashed", color="magenta", weight=3];
5479 -> 5545[label="",style="dashed", color="magenta", weight=3];
5479 -> 5546[label="",style="dashed", color="magenta", weight=3];
3686 -> 3701[label="",style="dashed", color="red", weight=0];
3686[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Pos Zero) (primMulInt (Pos (primMulNat (Succ yu220) (Succ Zero))) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="magenta"];3686 -> 3702[label="",style="dashed", color="magenta", weight=3];
3687 -> 3703[label="",style="dashed", color="red", weight=0];
3687[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Neg Zero) (primMulInt (Pos (primMulNat (Succ yu220) (Succ Zero))) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="magenta"];3687 -> 3704[label="",style="dashed", color="magenta", weight=3];
5568 -> 5537[label="",style="dashed", color="red", weight=0];
5568[label="primDivNatS (primMinusNatS yu5020 yu5030) (Succ yu504)",fontsize=16,color="magenta"];5568 -> 5572[label="",style="dashed", color="magenta", weight=3];
5568 -> 5573[label="",style="dashed", color="magenta", weight=3];
5569 -> 5463[label="",style="dashed", color="red", weight=0];
5569[label="primDivNatS (Succ yu5020) (Succ yu504)",fontsize=16,color="magenta"];5569 -> 5574[label="",style="dashed", color="magenta", weight=3];
5569 -> 5575[label="",style="dashed", color="magenta", weight=3];
5570 -> 2524[label="",style="dashed", color="red", weight=0];
5570[label="primDivNatS Zero (Succ yu504)",fontsize=16,color="magenta"];5570 -> 5576[label="",style="dashed", color="magenta", weight=3];
5571 -> 2524[label="",style="dashed", color="red", weight=0];
5571[label="primDivNatS Zero (Succ yu504)",fontsize=16,color="magenta"];5571 -> 5577[label="",style="dashed", color="magenta", weight=3];
391 -> 2727[label="",style="dashed", color="red", weight=0];
391[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ (Succ yu31000)))) (primCmpInt (Pos Zero) (Pos (primMulNat (primMulNat (Succ (Succ yu31000)) (Succ Zero)) (Succ Zero))) == LT)",fontsize=16,color="magenta"];391 -> 2728[label="",style="dashed", color="magenta", weight=3];
391 -> 2729[label="",style="dashed", color="magenta", weight=3];
392[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primCmpInt (Pos Zero) (primMulInt (Pos (Succ Zero) * Pos (Succ Zero)) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];392 -> 457[label="",style="solid", color="black", weight=3];
1592 -> 1596[label="",style="dashed", color="red", weight=0];
1592[label="primPlusNat (primMulNat yu1120 (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];1592 -> 1597[label="",style="dashed", color="magenta", weight=3];
1593[label="Zero",fontsize=16,color="green",shape="box"];1500[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu71))) (LT == LT)\n  Integral a",fontsize=16,color="black",shape="box"];1500 -> 1516[label="",style="solid", color="black", weight=3];
1501[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu71))) False\n  Integral a",fontsize=16,color="black",shape="box"];1501 -> 1517[label="",style="solid", color="black", weight=3];
5262[label="yu47500",fontsize=16,color="green",shape="box"];5263[label="yu30000",fontsize=16,color="green",shape="box"];5264[label="yu481",fontsize=16,color="green",shape="box"];5265[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (primCmpInt (Pos Zero) (Neg (Succ yu4860)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5265 -> 5280[label="",style="solid", color="black", weight=3];
5266[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (primCmpInt (Pos Zero) (Neg Zero) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5266 -> 5281[label="",style="solid", color="black", weight=3];
1753[label="floorFloor0 (Float (Pos Zero) (Neg (Succ yu78))) False\n  Integral a",fontsize=16,color="black",shape="triangle"];1753 -> 1772[label="",style="solid", color="black", weight=3];
1754 -> 1753[label="",style="dashed", color="red", weight=0];
1754[label="floorFloor0 (Float (Pos Zero) (Neg (Succ yu78))) False\n  Integral a",fontsize=16,color="magenta"];5178 -> 1571[label="",style="dashed", color="red", weight=0];
5178[label="primMulNat yu472 (Succ Zero)",fontsize=16,color="magenta"];5178 -> 5191[label="",style="dashed", color="magenta", weight=3];
5177[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Pos Zero) (Pos yu477) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];5736[label="yu477/Succ yu4770",fontsize=10,color="white",style="solid",shape="box"];5177 -> 5736[label="",style="solid", color="burlywood", weight=9];
5736 -> 5192[label="",style="solid", color="burlywood", weight=3];
5737[label="yu477/Zero",fontsize=10,color="white",style="solid",shape="box"];5177 -> 5737[label="",style="solid", color="burlywood", weight=9];
5737 -> 5193[label="",style="solid", color="burlywood", weight=3];
5184 -> 1571[label="",style="dashed", color="red", weight=0];
5184[label="primMulNat yu473 (Succ Zero)",fontsize=16,color="magenta"];5184 -> 5194[label="",style="dashed", color="magenta", weight=3];
5183[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Neg Zero) (Pos yu478) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];5739[label="yu478/Succ yu4780",fontsize=10,color="white",style="solid",shape="box"];5183 -> 5739[label="",style="solid", color="burlywood", weight=9];
5739 -> 5195[label="",style="solid", color="burlywood", weight=3];
5740[label="yu478/Zero",fontsize=10,color="white",style="solid",shape="box"];5183 -> 5740[label="",style="solid", color="burlywood", weight=9];
5740 -> 5196[label="",style="solid", color="burlywood", weight=3];
1930[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu87))) (LT == LT)\n  Integral a",fontsize=16,color="black",shape="box"];1930 -> 1944[label="",style="solid", color="black", weight=3];
1931[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu87))) False\n  Integral a",fontsize=16,color="black",shape="box"];1931 -> 1945[label="",style="solid", color="black", weight=3];
5267[label="yu482",fontsize=16,color="green",shape="box"];5268[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (primCmpInt (Neg Zero) (Neg (Succ yu4870)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5268 -> 5282[label="",style="solid", color="black", weight=3];
5269[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (primCmpInt (Neg Zero) (Neg Zero) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5269 -> 5283[label="",style="solid", color="black", weight=3];
2156[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu94))) (GT == LT)\n  Integral a",fontsize=16,color="black",shape="box"];2156 -> 2172[label="",style="solid", color="black", weight=3];
2157[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu94))) False\n  Integral a",fontsize=16,color="black",shape="triangle"];2157 -> 2173[label="",style="solid", color="black", weight=3];
5544[label="Succ yu497",fontsize=16,color="green",shape="box"];5545[label="Succ yu498",fontsize=16,color="green",shape="box"];5546[label="Succ yu498",fontsize=16,color="green",shape="box"];3702 -> 1571[label="",style="dashed", color="red", weight=0];
3702[label="primMulNat (Succ yu220) (Succ Zero)",fontsize=16,color="magenta"];3702 -> 3716[label="",style="dashed", color="magenta", weight=3];
3701[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Pos Zero) (primMulInt (Pos yu374) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];3701 -> 3717[label="",style="solid", color="black", weight=3];
3704 -> 1571[label="",style="dashed", color="red", weight=0];
3704[label="primMulNat (Succ yu220) (Succ Zero)",fontsize=16,color="magenta"];3704 -> 3718[label="",style="dashed", color="magenta", weight=3];
3703[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Neg Zero) (primMulInt (Pos yu375) (Pos (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];3703 -> 3719[label="",style="solid", color="black", weight=3];
5572[label="yu5020",fontsize=16,color="green",shape="box"];5573[label="yu5030",fontsize=16,color="green",shape="box"];5574[label="yu5020",fontsize=16,color="green",shape="box"];5575[label="yu504",fontsize=16,color="green",shape="box"];5463[label="primDivNatS (Succ yu449) (Succ yu450)",fontsize=16,color="black",shape="triangle"];5463 -> 5470[label="",style="solid", color="black", weight=3];
5576[label="yu504",fontsize=16,color="green",shape="box"];2524[label="primDivNatS Zero (Succ yu71)",fontsize=16,color="black",shape="triangle"];2524 -> 2779[label="",style="solid", color="black", weight=3];
5577[label="yu504",fontsize=16,color="green",shape="box"];2728 -> 1571[label="",style="dashed", color="red", weight=0];
2728[label="primMulNat (primMulNat (Succ (Succ yu31000)) (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];2728 -> 2773[label="",style="dashed", color="magenta", weight=3];
2729[label="Succ yu31000",fontsize=16,color="green",shape="box"];2727[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ yu283))) (primCmpInt (Pos Zero) (Pos yu326) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];5744[label="yu326/Succ yu3260",fontsize=10,color="white",style="solid",shape="box"];2727 -> 5744[label="",style="solid", color="burlywood", weight=9];
5744 -> 2774[label="",style="solid", color="burlywood", weight=3];
5745[label="yu326/Zero",fontsize=10,color="white",style="solid",shape="box"];2727 -> 5745[label="",style="solid", color="burlywood", weight=9];
5745 -> 2775[label="",style="solid", color="burlywood", weight=3];
457[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primCmpInt (Pos Zero) (primMulInt (primMulInt (Pos (Succ Zero)) (Pos (Succ Zero))) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];457 -> 528[label="",style="solid", color="black", weight=3];
1597 -> 1571[label="",style="dashed", color="red", weight=0];
1597[label="primMulNat yu1120 (Succ Zero)",fontsize=16,color="magenta"];1597 -> 1611[label="",style="dashed", color="magenta", weight=3];
1596[label="primPlusNat yu116 (Succ Zero)",fontsize=16,color="burlywood",shape="triangle"];5747[label="yu116/Succ yu1160",fontsize=10,color="white",style="solid",shape="box"];1596 -> 5747[label="",style="solid", color="burlywood", weight=9];
5747 -> 1612[label="",style="solid", color="burlywood", weight=3];
5748[label="yu116/Zero",fontsize=10,color="white",style="solid",shape="box"];1596 -> 5748[label="",style="solid", color="burlywood", weight=9];
5748 -> 1613[label="",style="solid", color="burlywood", weight=3];
1516[label="floorFloor0 (Float (Pos Zero) (Pos (Succ yu71))) True\n  Integral a",fontsize=16,color="black",shape="box"];1516 -> 1531[label="",style="solid", color="black", weight=3];
1517[label="floorN (Float (Pos Zero) (Pos (Succ yu71)))\n  Integral a",fontsize=16,color="black",shape="triangle"];1517 -> 1532[label="",style="solid", color="black", weight=3];
5280[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (GT == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5280 -> 5295[label="",style="solid", color="black", weight=3];
5281[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (EQ == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5281 -> 5296[label="",style="solid", color="black", weight=3];
1772[label="floorN (Float (Pos Zero) (Neg (Succ yu78)))\n  Integral a",fontsize=16,color="black",shape="box"];1772 -> 1778[label="",style="solid", color="black", weight=3];
5191[label="yu472",fontsize=16,color="green",shape="box"];5192[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Pos Zero) (Pos (Succ yu4770)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5192 -> 5215[label="",style="solid", color="black", weight=3];
5193[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Pos Zero) (Pos Zero) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5193 -> 5216[label="",style="solid", color="black", weight=3];
5194[label="yu473",fontsize=16,color="green",shape="box"];5195[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Neg Zero) (Pos (Succ yu4780)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5195 -> 5217[label="",style="solid", color="black", weight=3];
5196[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpInt (Neg Zero) (Pos Zero) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5196 -> 5218[label="",style="solid", color="black", weight=3];
1944[label="floorFloor0 (Float (Neg Zero) (Pos (Succ yu87))) True\n  Integral a",fontsize=16,color="black",shape="box"];1944 -> 1958[label="",style="solid", color="black", weight=3];
1945[label="floorN (Float (Neg Zero) (Pos (Succ yu87)))\n  Integral a",fontsize=16,color="black",shape="triangle"];1945 -> 1959[label="",style="solid", color="black", weight=3];
5282[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (primCmpNat (Succ yu4870) Zero == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5282 -> 5297[label="",style="solid", color="black", weight=3];
5283[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (EQ == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5283 -> 5298[label="",style="solid", color="black", weight=3];
2172 -> 2157[label="",style="dashed", color="red", weight=0];
2172[label="floorFloor0 (Float (Neg Zero) (Neg (Succ yu94))) False\n  Integral a",fontsize=16,color="magenta"];2173[label="floorN (Float (Neg Zero) (Neg (Succ yu94)))\n  Integral a",fontsize=16,color="black",shape="box"];2173 -> 2181[label="",style="solid", color="black", weight=3];
3716[label="Succ yu220",fontsize=16,color="green",shape="box"];3717 -> 3746[label="",style="dashed", color="red", weight=0];
3717[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Pos Zero) (Pos (primMulNat yu374 (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="magenta"];3717 -> 3747[label="",style="dashed", color="magenta", weight=3];
3718[label="Succ yu220",fontsize=16,color="green",shape="box"];3719 -> 3748[label="",style="dashed", color="red", weight=0];
3719[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Neg Zero) (Pos (primMulNat yu375 (Succ Zero))) == LT)\n  Integral a",fontsize=16,color="magenta"];3719 -> 3749[label="",style="dashed", color="magenta", weight=3];
5470 -> 4878[label="",style="dashed", color="red", weight=0];
5470[label="primDivNatS0 yu449 yu450 (primGEqNatS yu449 yu450)",fontsize=16,color="magenta"];5470 -> 5477[label="",style="dashed", color="magenta", weight=3];
5470 -> 5478[label="",style="dashed", color="magenta", weight=3];
2779[label="Zero",fontsize=16,color="green",shape="box"];2773 -> 1571[label="",style="dashed", color="red", weight=0];
2773[label="primMulNat (Succ (Succ yu31000)) (Succ Zero)",fontsize=16,color="magenta"];2773 -> 2788[label="",style="dashed", color="magenta", weight=3];
2774[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ yu283))) (primCmpInt (Pos Zero) (Pos (Succ yu3260)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];2774 -> 2789[label="",style="solid", color="black", weight=3];
2775[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ yu283))) (primCmpInt (Pos Zero) (Pos Zero) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];2775 -> 2790[label="",style="solid", color="black", weight=3];
528[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primCmpInt (Pos Zero) (primMulInt (Pos (primMulNat (Succ Zero) (Succ Zero))) (Pos (Succ Zero))) == LT)",fontsize=16,color="black",shape="box"];528 -> 614[label="",style="solid", color="black", weight=3];
1611[label="yu1120",fontsize=16,color="green",shape="box"];1612[label="primPlusNat (Succ yu1160) (Succ Zero)",fontsize=16,color="black",shape="box"];1612 -> 1631[label="",style="solid", color="black", weight=3];
1613[label="primPlusNat Zero (Succ Zero)",fontsize=16,color="black",shape="box"];1613 -> 1632[label="",style="solid", color="black", weight=3];
1531[label="floorN (Float (Pos Zero) (Pos (Succ yu71))) - fromInt (Pos (Succ Zero))\n  Integral a",fontsize=16,color="blue",shape="box"];5754[label="- :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];1531 -> 5754[label="",style="solid", color="blue", weight=9];
5754 -> 1566[label="",style="solid", color="blue", weight=3];
5755[label="- :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1531 -> 5755[label="",style="solid", color="blue", weight=9];
5755 -> 1567[label="",style="solid", color="blue", weight=3];
1532[label="floorN0 (Float (Pos Zero) (Pos (Succ yu71))) (floorVu9 (Float (Pos Zero) (Pos (Succ yu71))))\n  Integral a",fontsize=16,color="black",shape="box"];1532 -> 1551[label="",style="solid", color="black", weight=3];
5295[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) False\n  Integral a",fontsize=16,color="black",shape="triangle"];5295 -> 5306[label="",style="solid", color="black", weight=3];
5296 -> 5295[label="",style="dashed", color="red", weight=0];
5296[label="floorFloor0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) False\n  Integral a",fontsize=16,color="magenta"];1778[label="floorN0 (Float (Pos Zero) (Neg (Succ yu78))) (floorVu9 (Float (Pos Zero) (Neg (Succ yu78))))\n  Integral a",fontsize=16,color="black",shape="box"];1778 -> 1782[label="",style="solid", color="black", weight=3];
5215[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (primCmpNat Zero (Succ yu4770) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5215 -> 5270[label="",style="solid", color="black", weight=3];
5216[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (EQ == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];5216 -> 5271[label="",style="solid", color="black", weight=3];
5217[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (LT == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];5217 -> 5272[label="",style="solid", color="black", weight=3];
5218 -> 5216[label="",style="dashed", color="red", weight=0];
5218[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (EQ == LT)\n  Integral a",fontsize=16,color="magenta"];1958[label="floorN (Float (Neg Zero) (Pos (Succ yu87))) - fromInt (Pos (Succ Zero))\n  Integral a",fontsize=16,color="blue",shape="box"];5758[label="- :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];1958 -> 5758[label="",style="solid", color="blue", weight=9];
5758 -> 1984[label="",style="solid", color="blue", weight=3];
5759[label="- :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1958 -> 5759[label="",style="solid", color="blue", weight=9];
5759 -> 1985[label="",style="solid", color="blue", weight=3];
1959[label="floorN0 (Float (Neg Zero) (Pos (Succ yu87))) (floorVu9 (Float (Neg Zero) (Pos (Succ yu87))))\n  Integral a",fontsize=16,color="black",shape="box"];1959 -> 1976[label="",style="solid", color="black", weight=3];
5297[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (GT == LT)\n  Integral a",fontsize=16,color="black",shape="box"];5297 -> 5307[label="",style="solid", color="black", weight=3];
5298[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) False\n  Integral a",fontsize=16,color="black",shape="triangle"];5298 -> 5308[label="",style="solid", color="black", weight=3];
2181[label="floorN0 (Float (Neg Zero) (Neg (Succ yu94))) (floorVu9 (Float (Neg Zero) (Neg (Succ yu94))))\n  Integral a",fontsize=16,color="black",shape="box"];2181 -> 2190[label="",style="solid", color="black", weight=3];
3747 -> 1571[label="",style="dashed", color="red", weight=0];
3747[label="primMulNat yu374 (Succ Zero)",fontsize=16,color="magenta"];3747 -> 3764[label="",style="dashed", color="magenta", weight=3];
3746[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Pos Zero) (Pos yu377) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];5761[label="yu377/Succ yu3770",fontsize=10,color="white",style="solid",shape="box"];3746 -> 5761[label="",style="solid", color="burlywood", weight=9];
5761 -> 3765[label="",style="solid", color="burlywood", weight=3];
5762[label="yu377/Zero",fontsize=10,color="white",style="solid",shape="box"];3746 -> 5762[label="",style="solid", color="burlywood", weight=9];
5762 -> 3766[label="",style="solid", color="burlywood", weight=3];
3749 -> 1571[label="",style="dashed", color="red", weight=0];
3749[label="primMulNat yu375 (Succ Zero)",fontsize=16,color="magenta"];3749 -> 3767[label="",style="dashed", color="magenta", weight=3];
3748[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Neg Zero) (Pos yu378) == LT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];5764[label="yu378/Succ yu3780",fontsize=10,color="white",style="solid",shape="box"];3748 -> 5764[label="",style="solid", color="burlywood", weight=9];
5764 -> 3768[label="",style="solid", color="burlywood", weight=3];
5765[label="yu378/Zero",fontsize=10,color="white",style="solid",shape="box"];3748 -> 5765[label="",style="solid", color="burlywood", weight=9];
5765 -> 3769[label="",style="solid", color="burlywood", weight=3];
5477[label="yu450",fontsize=16,color="green",shape="box"];5478[label="yu449",fontsize=16,color="green",shape="box"];2788[label="Succ (Succ yu31000)",fontsize=16,color="green",shape="box"];2789[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ yu283))) (primCmpNat Zero (Succ yu3260) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];2789 -> 2799[label="",style="solid", color="black", weight=3];
2790[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ yu283))) (EQ == LT)\n  Integral a",fontsize=16,color="black",shape="box"];2790 -> 2800[label="",style="solid", color="black", weight=3];
614 -> 2727[label="",style="dashed", color="red", weight=0];
614[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primCmpInt (Pos Zero) (Pos (primMulNat (primMulNat (Succ Zero) (Succ Zero)) (Succ Zero))) == LT)",fontsize=16,color="magenta"];614 -> 2734[label="",style="dashed", color="magenta", weight=3];
614 -> 2735[label="",style="dashed", color="magenta", weight=3];
1631[label="Succ (Succ (primPlusNat yu1160 Zero))",fontsize=16,color="green",shape="box"];1631 -> 1713[label="",style="dashed", color="green", weight=3];
1632[label="Succ Zero",fontsize=16,color="green",shape="box"];1566[label="floorN (Float (Pos Zero) (Pos (Succ yu71))) - fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1566 -> 1986[label="",style="solid", color="black", weight=3];
1567[label="floorN (Float (Pos Zero) (Pos (Succ yu71))) - fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1567 -> 1987[label="",style="solid", color="black", weight=3];
1551[label="floorN0 (Float (Pos Zero) (Pos (Succ yu71))) (properFraction (Float (Pos Zero) (Pos (Succ yu71))))\n  Integral a",fontsize=16,color="black",shape="box"];1551 -> 1568[label="",style="solid", color="black", weight=3];
5306[label="floorN (Float (Pos (Succ yu463)) (Neg (Succ yu464)))\n  Integral a",fontsize=16,color="black",shape="box"];5306 -> 5323[label="",style="solid", color="black", weight=3];
1782[label="floorN0 (Float (Pos Zero) (Neg (Succ yu78))) (properFraction (Float (Pos Zero) (Neg (Succ yu78))))\n  Integral a",fontsize=16,color="black",shape="box"];1782 -> 1791[label="",style="solid", color="black", weight=3];
5270 -> 5217[label="",style="dashed", color="red", weight=0];
5270[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (LT == LT)\n  Integral a",fontsize=16,color="magenta"];5271[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) False\n  Integral a",fontsize=16,color="black",shape="box"];5271 -> 5284[label="",style="solid", color="black", weight=3];
5272[label="floorFloor0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) True\n  Integral a",fontsize=16,color="black",shape="box"];5272 -> 5285[label="",style="solid", color="black", weight=3];
1984[label="floorN (Float (Neg Zero) (Pos (Succ yu87))) - fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1984 -> 2924[label="",style="solid", color="black", weight=3];
1985[label="floorN (Float (Neg Zero) (Pos (Succ yu87))) - fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1985 -> 2925[label="",style="solid", color="black", weight=3];
1976[label="floorN0 (Float (Neg Zero) (Pos (Succ yu87))) (properFraction (Float (Neg Zero) (Pos (Succ yu87))))\n  Integral a",fontsize=16,color="black",shape="box"];1976 -> 1988[label="",style="solid", color="black", weight=3];
5307 -> 5298[label="",style="dashed", color="red", weight=0];
5307[label="floorFloor0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) False\n  Integral a",fontsize=16,color="magenta"];5308[label="floorN (Float (Neg (Succ yu468)) (Neg (Succ yu469)))\n  Integral a",fontsize=16,color="black",shape="box"];5308 -> 5324[label="",style="solid", color="black", weight=3];
2190[label="floorN0 (Float (Neg Zero) (Neg (Succ yu94))) (properFraction (Float (Neg Zero) (Neg (Succ yu94))))\n  Integral a",fontsize=16,color="black",shape="box"];2190 -> 2199[label="",style="solid", color="black", weight=3];
3764[label="yu374",fontsize=16,color="green",shape="box"];3765[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Pos Zero) (Pos (Succ yu3770)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];3765 -> 3822[label="",style="solid", color="black", weight=3];
3766[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Pos Zero) (Pos Zero) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];3766 -> 3823[label="",style="solid", color="black", weight=3];
3767[label="yu375",fontsize=16,color="green",shape="box"];3768[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Neg Zero) (Pos (Succ yu3780)) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];3768 -> 3824[label="",style="solid", color="black", weight=3];
3769[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpInt (Neg Zero) (Pos Zero) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];3769 -> 3825[label="",style="solid", color="black", weight=3];
2799[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ yu283))) (LT == LT)\n  Integral a",fontsize=16,color="black",shape="box"];2799 -> 2803[label="",style="solid", color="black", weight=3];
2800[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ yu283))) False\n  Integral a",fontsize=16,color="black",shape="box"];2800 -> 2804[label="",style="solid", color="black", weight=3];
2734 -> 1571[label="",style="dashed", color="red", weight=0];
2734[label="primMulNat (primMulNat (Succ Zero) (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];2734 -> 2776[label="",style="dashed", color="magenta", weight=3];
2735[label="Zero",fontsize=16,color="green",shape="box"];1713[label="primPlusNat yu1160 Zero",fontsize=16,color="burlywood",shape="triangle"];5770[label="yu1160/Succ yu11600",fontsize=10,color="white",style="solid",shape="box"];1713 -> 5770[label="",style="solid", color="burlywood", weight=9];
5770 -> 1736[label="",style="solid", color="burlywood", weight=3];
5771[label="yu1160/Zero",fontsize=10,color="white",style="solid",shape="box"];1713 -> 5771[label="",style="solid", color="burlywood", weight=9];
5771 -> 1737[label="",style="solid", color="burlywood", weight=3];
1986[label="error []",fontsize=16,color="red",shape="box"];1987 -> 2002[label="",style="dashed", color="red", weight=0];
1987[label="primMinusInt (floorN (Float (Pos Zero) (Pos (Succ yu71)))) (fromInt (Pos (Succ Zero)))",fontsize=16,color="magenta"];1987 -> 2003[label="",style="dashed", color="magenta", weight=3];
1568[label="floorN0 (Float (Pos Zero) (Pos (Succ yu71))) (floatProperFractionFloat (Float (Pos Zero) (Pos (Succ yu71))))\n  Integral a",fontsize=16,color="black",shape="box"];1568 -> 1616[label="",style="solid", color="black", weight=3];
5323[label="floorN0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (floorVu9 (Float (Pos (Succ yu463)) (Neg (Succ yu464))))\n  Integral a",fontsize=16,color="black",shape="box"];5323 -> 5339[label="",style="solid", color="black", weight=3];
1791[label="floorN0 (Float (Pos Zero) (Neg (Succ yu78))) (floatProperFractionFloat (Float (Pos Zero) (Neg (Succ yu78))))\n  Integral a",fontsize=16,color="black",shape="box"];1791 -> 1794[label="",style="solid", color="black", weight=3];
5284[label="floorN (Float (Neg (Succ yu449)) (Pos (Succ yu450)))\n  Integral a",fontsize=16,color="black",shape="triangle"];5284 -> 5299[label="",style="solid", color="black", weight=3];
5285[label="floorN (Float (Neg (Succ yu449)) (Pos (Succ yu450))) - fromInt (Pos (Succ Zero))\n  Integral a",fontsize=16,color="blue",shape="box"];5773[label="- :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];5285 -> 5773[label="",style="solid", color="blue", weight=9];
5773 -> 5326[label="",style="solid", color="blue", weight=3];
5774[label="- :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];5285 -> 5774[label="",style="solid", color="blue", weight=9];
5774 -> 5327[label="",style="solid", color="blue", weight=3];
2924[label="error []",fontsize=16,color="red",shape="box"];2925 -> 2002[label="",style="dashed", color="red", weight=0];
2925[label="primMinusInt (floorN (Float (Neg Zero) (Pos (Succ yu87)))) (fromInt (Pos (Succ Zero)))",fontsize=16,color="magenta"];2925 -> 2941[label="",style="dashed", color="magenta", weight=3];
1988[label="floorN0 (Float (Neg Zero) (Pos (Succ yu87))) (floatProperFractionFloat (Float (Neg Zero) (Pos (Succ yu87))))\n  Integral a",fontsize=16,color="black",shape="box"];1988 -> 2006[label="",style="solid", color="black", weight=3];
5324[label="floorN0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (floorVu9 (Float (Neg (Succ yu468)) (Neg (Succ yu469))))\n  Integral a",fontsize=16,color="black",shape="box"];5324 -> 5340[label="",style="solid", color="black", weight=3];
2199[label="floorN0 (Float (Neg Zero) (Neg (Succ yu94))) (floatProperFractionFloat (Float (Neg Zero) (Neg (Succ yu94))))\n  Integral a",fontsize=16,color="black",shape="box"];2199 -> 2208[label="",style="solid", color="black", weight=3];
3822[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (primCmpNat Zero (Succ yu3770) == LT)\n  Integral a",fontsize=16,color="black",shape="box"];3822 -> 3858[label="",style="solid", color="black", weight=3];
3823[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (EQ == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];3823 -> 3859[label="",style="solid", color="black", weight=3];
3824[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (LT == LT)\n  Integral a",fontsize=16,color="black",shape="triangle"];3824 -> 3860[label="",style="solid", color="black", weight=3];
3825 -> 3823[label="",style="dashed", color="red", weight=0];
3825[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (EQ == LT)\n  Integral a",fontsize=16,color="magenta"];2803[label="floorFloor0 (Float (Pos (Succ Zero)) (Pos (Succ yu283))) True\n  Integral a",fontsize=16,color="black",shape="box"];2803 -> 2879[label="",style="solid", color="black", weight=3];
2804[label="floorN (Float (Pos (Succ Zero)) (Pos (Succ yu283)))\n  Integral a",fontsize=16,color="black",shape="triangle"];2804 -> 2880[label="",style="solid", color="black", weight=3];
2776 -> 1571[label="",style="dashed", color="red", weight=0];
2776[label="primMulNat (Succ Zero) (Succ Zero)",fontsize=16,color="magenta"];2776 -> 2791[label="",style="dashed", color="magenta", weight=3];
1736[label="primPlusNat (Succ yu11600) Zero",fontsize=16,color="black",shape="box"];1736 -> 1755[label="",style="solid", color="black", weight=3];
1737[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];1737 -> 1756[label="",style="solid", color="black", weight=3];
2003 -> 1517[label="",style="dashed", color="red", weight=0];
2003[label="floorN (Float (Pos Zero) (Pos (Succ yu71)))",fontsize=16,color="magenta"];2002[label="primMinusInt yu193 (fromInt (Pos (Succ Zero)))",fontsize=16,color="burlywood",shape="triangle"];5779[label="yu193/Pos yu1930",fontsize=10,color="white",style="solid",shape="box"];2002 -> 5779[label="",style="solid", color="burlywood", weight=9];
5779 -> 2010[label="",style="solid", color="burlywood", weight=3];
5780[label="yu193/Neg yu1930",fontsize=10,color="white",style="solid",shape="box"];2002 -> 5780[label="",style="solid", color="burlywood", weight=9];
5780 -> 2011[label="",style="solid", color="burlywood", weight=3];
1616[label="floorN0 (Float (Pos Zero) (Pos (Succ yu71))) (fromInt (Pos Zero `quot` Pos (Succ yu71)),Float (Pos Zero) (Pos (Succ yu71)) - fromInt (Pos Zero `quot` Pos (Succ yu71)))\n  Integral a",fontsize=16,color="black",shape="box"];1616 -> 1635[label="",style="solid", color="black", weight=3];
5339[label="floorN0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (properFraction (Float (Pos (Succ yu463)) (Neg (Succ yu464))))\n  Integral a",fontsize=16,color="black",shape="box"];5339 -> 5355[label="",style="solid", color="black", weight=3];
1794[label="floorN0 (Float (Pos Zero) (Neg (Succ yu78))) (fromInt (Pos Zero `quot` Neg (Succ yu78)),Float (Pos Zero) (Neg (Succ yu78)) - fromInt (Pos Zero `quot` Neg (Succ yu78)))\n  Integral a",fontsize=16,color="black",shape="box"];1794 -> 1797[label="",style="solid", color="black", weight=3];
5299[label="floorN0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (floorVu9 (Float (Neg (Succ yu449)) (Pos (Succ yu450))))\n  Integral a",fontsize=16,color="black",shape="box"];5299 -> 5309[label="",style="solid", color="black", weight=3];
5326 -> 5310[label="",style="dashed", color="red", weight=0];
5326[label="floorN (Float (Neg (Succ yu449)) (Pos (Succ yu450))) - fromInt (Pos (Succ Zero))",fontsize=16,color="magenta"];5326 -> 5342[label="",style="dashed", color="magenta", weight=3];
5327 -> 5311[label="",style="dashed", color="red", weight=0];
5327[label="floorN (Float (Neg (Succ yu449)) (Pos (Succ yu450))) - fromInt (Pos (Succ Zero))",fontsize=16,color="magenta"];5327 -> 5343[label="",style="dashed", color="magenta", weight=3];
2941 -> 1945[label="",style="dashed", color="red", weight=0];
2941[label="floorN (Float (Neg Zero) (Pos (Succ yu87)))",fontsize=16,color="magenta"];2006[label="floorN0 (Float (Neg Zero) (Pos (Succ yu87))) (fromInt (Neg Zero `quot` Pos (Succ yu87)),Float (Neg Zero) (Pos (Succ yu87)) - fromInt (Neg Zero `quot` Pos (Succ yu87)))\n  Integral a",fontsize=16,color="black",shape="box"];2006 -> 2018[label="",style="solid", color="black", weight=3];
5340[label="floorN0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (properFraction (Float (Neg (Succ yu468)) (Neg (Succ yu469))))\n  Integral a",fontsize=16,color="black",shape="box"];5340 -> 5356[label="",style="solid", color="black", weight=3];
2208[label="floorN0 (Float (Neg Zero) (Neg (Succ yu94))) (fromInt (Neg Zero `quot` Neg (Succ yu94)),Float (Neg Zero) (Neg (Succ yu94)) - fromInt (Neg Zero `quot` Neg (Succ yu94)))\n  Integral a",fontsize=16,color="black",shape="box"];2208 -> 2222[label="",style="solid", color="black", weight=3];
3858 -> 3824[label="",style="dashed", color="red", weight=0];
3858[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (LT == LT)\n  Integral a",fontsize=16,color="magenta"];3859[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) False\n  Integral a",fontsize=16,color="black",shape="box"];3859 -> 3927[label="",style="solid", color="black", weight=3];
3860[label="floorFloor0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) True\n  Integral a",fontsize=16,color="black",shape="box"];3860 -> 3928[label="",style="solid", color="black", weight=3];
2879[label="floorN (Float (Pos (Succ Zero)) (Pos (Succ yu283))) - fromInt (Pos (Succ Zero))\n  Integral a",fontsize=16,color="blue",shape="box"];5785[label="- :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];2879 -> 5785[label="",style="solid", color="blue", weight=9];
5785 -> 2927[label="",style="solid", color="blue", weight=3];
5786[label="- :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];2879 -> 5786[label="",style="solid", color="blue", weight=9];
5786 -> 2928[label="",style="solid", color="blue", weight=3];
2880[label="floorN0 (Float (Pos (Succ Zero)) (Pos (Succ yu283))) (floorVu9 (Float (Pos (Succ Zero)) (Pos (Succ yu283))))\n  Integral a",fontsize=16,color="black",shape="box"];2880 -> 2909[label="",style="solid", color="black", weight=3];
2791[label="Succ Zero",fontsize=16,color="green",shape="box"];1755[label="Succ yu11600",fontsize=16,color="green",shape="box"];1756[label="Zero",fontsize=16,color="green",shape="box"];2010[label="primMinusInt (Pos yu1930) (fromInt (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];2010 -> 2022[label="",style="solid", color="black", weight=3];
2011[label="primMinusInt (Neg yu1930) (fromInt (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];2011 -> 2023[label="",style="solid", color="black", weight=3];
1635[label="fromInt (Pos Zero `quot` Pos (Succ yu71))\n  Integral a",fontsize=16,color="blue",shape="box"];5787[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];1635 -> 5787[label="",style="solid", color="blue", weight=9];
5787 -> 1716[label="",style="solid", color="blue", weight=3];
5788[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1635 -> 5788[label="",style="solid", color="blue", weight=9];
5788 -> 1717[label="",style="solid", color="blue", weight=3];
5355[label="floorN0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (floatProperFractionFloat (Float (Pos (Succ yu463)) (Neg (Succ yu464))))\n  Integral a",fontsize=16,color="black",shape="box"];5355 -> 5370[label="",style="solid", color="black", weight=3];
1797[label="fromInt (Pos Zero `quot` Neg (Succ yu78))\n  Integral a",fontsize=16,color="blue",shape="box"];5789[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];1797 -> 5789[label="",style="solid", color="blue", weight=9];
5789 -> 1810[label="",style="solid", color="blue", weight=3];
5790[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1797 -> 5790[label="",style="solid", color="blue", weight=9];
5790 -> 1811[label="",style="solid", color="blue", weight=3];
5309[label="floorN0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (properFraction (Float (Neg (Succ yu449)) (Pos (Succ yu450))))\n  Integral a",fontsize=16,color="black",shape="box"];5309 -> 5325[label="",style="solid", color="black", weight=3];
5342 -> 5284[label="",style="dashed", color="red", weight=0];
5342[label="floorN (Float (Neg (Succ yu449)) (Pos (Succ yu450)))",fontsize=16,color="magenta"];5310[label="yu491 - fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="triangle"];5310 -> 5328[label="",style="solid", color="black", weight=3];
5343 -> 5284[label="",style="dashed", color="red", weight=0];
5343[label="floorN (Float (Neg (Succ yu449)) (Pos (Succ yu450)))",fontsize=16,color="magenta"];5311[label="yu491 - fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="triangle"];5311 -> 5329[label="",style="solid", color="black", weight=3];
2018[label="fromInt (Neg Zero `quot` Pos (Succ yu87))\n  Integral a",fontsize=16,color="blue",shape="box"];5793[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];2018 -> 5793[label="",style="solid", color="blue", weight=9];
5793 -> 2026[label="",style="solid", color="blue", weight=3];
5794[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];2018 -> 5794[label="",style="solid", color="blue", weight=9];
5794 -> 2027[label="",style="solid", color="blue", weight=3];
5356[label="floorN0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (floatProperFractionFloat (Float (Neg (Succ yu468)) (Neg (Succ yu469))))\n  Integral a",fontsize=16,color="black",shape="box"];5356 -> 5371[label="",style="solid", color="black", weight=3];
2222[label="fromInt (Neg Zero `quot` Neg (Succ yu94))\n  Integral a",fontsize=16,color="blue",shape="box"];5795[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];2222 -> 5795[label="",style="solid", color="blue", weight=9];
5795 -> 2244[label="",style="solid", color="blue", weight=3];
5796[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];2222 -> 5796[label="",style="solid", color="blue", weight=9];
5796 -> 2245[label="",style="solid", color="blue", weight=3];
3927[label="floorN (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220)))\n  Integral a",fontsize=16,color="black",shape="triangle"];3927 -> 3948[label="",style="solid", color="black", weight=3];
3928[label="floorN (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) - fromInt (Pos (Succ Zero))\n  Integral a",fontsize=16,color="blue",shape="box"];5797[label="- :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];3928 -> 5797[label="",style="solid", color="blue", weight=9];
5797 -> 4060[label="",style="solid", color="blue", weight=3];
5798[label="- :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];3928 -> 5798[label="",style="solid", color="blue", weight=9];
5798 -> 4061[label="",style="solid", color="blue", weight=3];
2927[label="floorN (Float (Pos (Succ Zero)) (Pos (Succ yu283))) - fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];2927 -> 4062[label="",style="solid", color="black", weight=3];
2928[label="floorN (Float (Pos (Succ Zero)) (Pos (Succ yu283))) - fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];2928 -> 4063[label="",style="solid", color="black", weight=3];
2909[label="floorN0 (Float (Pos (Succ Zero)) (Pos (Succ yu283))) (properFraction (Float (Pos (Succ Zero)) (Pos (Succ yu283))))\n  Integral a",fontsize=16,color="black",shape="box"];2909 -> 2929[label="",style="solid", color="black", weight=3];
2022[label="primMinusInt (Pos yu1930) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];2022 -> 2030[label="",style="solid", color="black", weight=3];
2023[label="primMinusInt (Neg yu1930) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];2023 -> 2031[label="",style="solid", color="black", weight=3];
1716[label="fromInt (Pos Zero `quot` Pos (Succ yu71))",fontsize=16,color="black",shape="box"];1716 -> 1740[label="",style="solid", color="black", weight=3];
1717[label="fromInt (Pos Zero `quot` Pos (Succ yu71))",fontsize=16,color="black",shape="box"];1717 -> 1741[label="",style="solid", color="black", weight=3];
5370[label="floorN0 (Float (Pos (Succ yu463)) (Neg (Succ yu464))) (fromInt (Pos (Succ yu463) `quot` Neg (Succ yu464)),Float (Pos (Succ yu463)) (Neg (Succ yu464)) - fromInt (Pos (Succ yu463) `quot` Neg (Succ yu464)))\n  Integral a",fontsize=16,color="black",shape="box"];5370 -> 5383[label="",style="solid", color="black", weight=3];
1810[label="fromInt (Pos Zero `quot` Neg (Succ yu78))",fontsize=16,color="black",shape="box"];1810 -> 1825[label="",style="solid", color="black", weight=3];
1811[label="fromInt (Pos Zero `quot` Neg (Succ yu78))",fontsize=16,color="black",shape="box"];1811 -> 1826[label="",style="solid", color="black", weight=3];
5325[label="floorN0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (floatProperFractionFloat (Float (Neg (Succ yu449)) (Pos (Succ yu450))))\n  Integral a",fontsize=16,color="black",shape="box"];5325 -> 5341[label="",style="solid", color="black", weight=3];
5328[label="error []",fontsize=16,color="red",shape="box"];5329 -> 2002[label="",style="dashed", color="red", weight=0];
5329[label="primMinusInt yu491 (fromInt (Pos (Succ Zero)))",fontsize=16,color="magenta"];5329 -> 5344[label="",style="dashed", color="magenta", weight=3];
2026[label="fromInt (Neg Zero `quot` Pos (Succ yu87))",fontsize=16,color="black",shape="box"];2026 -> 2044[label="",style="solid", color="black", weight=3];
2027[label="fromInt (Neg Zero `quot` Pos (Succ yu87))",fontsize=16,color="black",shape="box"];2027 -> 2045[label="",style="solid", color="black", weight=3];
5371[label="floorN0 (Float (Neg (Succ yu468)) (Neg (Succ yu469))) (fromInt (Neg (Succ yu468) `quot` Neg (Succ yu469)),Float (Neg (Succ yu468)) (Neg (Succ yu469)) - fromInt (Neg (Succ yu468) `quot` Neg (Succ yu469)))\n  Integral a",fontsize=16,color="black",shape="box"];5371 -> 5384[label="",style="solid", color="black", weight=3];
2244[label="fromInt (Neg Zero `quot` Neg (Succ yu94))",fontsize=16,color="black",shape="box"];2244 -> 2254[label="",style="solid", color="black", weight=3];
2245[label="fromInt (Neg Zero `quot` Neg (Succ yu94))",fontsize=16,color="black",shape="box"];2245 -> 2255[label="",style="solid", color="black", weight=3];
3948[label="floorN0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (floorVu9 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))))\n  Integral a",fontsize=16,color="black",shape="box"];3948 -> 3976[label="",style="solid", color="black", weight=3];
4060[label="floorN (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) - fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];4060 -> 4489[label="",style="solid", color="black", weight=3];
4061[label="floorN (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) - fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];4061 -> 4490[label="",style="solid", color="black", weight=3];
4062[label="error []",fontsize=16,color="red",shape="box"];4063 -> 2002[label="",style="dashed", color="red", weight=0];
4063[label="primMinusInt (floorN (Float (Pos (Succ Zero)) (Pos (Succ yu283)))) (fromInt (Pos (Succ Zero)))",fontsize=16,color="magenta"];4063 -> 4141[label="",style="dashed", color="magenta", weight=3];
2929[label="floorN0 (Float (Pos (Succ Zero)) (Pos (Succ yu283))) (floatProperFractionFloat (Float (Pos (Succ Zero)) (Pos (Succ yu283))))\n  Integral a",fontsize=16,color="black",shape="box"];2929 -> 2951[label="",style="solid", color="black", weight=3];
2030[label="primMinusNat yu1930 (Succ Zero)",fontsize=16,color="burlywood",shape="triangle"];5801[label="yu1930/Succ yu19300",fontsize=10,color="white",style="solid",shape="box"];2030 -> 5801[label="",style="solid", color="burlywood", weight=9];
5801 -> 2048[label="",style="solid", color="burlywood", weight=3];
5802[label="yu1930/Zero",fontsize=10,color="white",style="solid",shape="box"];2030 -> 5802[label="",style="solid", color="burlywood", weight=9];
5802 -> 2049[label="",style="solid", color="burlywood", weight=3];
2031[label="Neg (primPlusNat yu1930 (Succ Zero))",fontsize=16,color="green",shape="box"];2031 -> 2050[label="",style="dashed", color="green", weight=3];
1740[label="Integer (Pos Zero `quot` Pos (Succ yu71))",fontsize=16,color="green",shape="box"];1740 -> 1763[label="",style="dashed", color="green", weight=3];
1741[label="Pos Zero `quot` Pos (Succ yu71)",fontsize=16,color="black",shape="triangle"];1741 -> 1764[label="",style="solid", color="black", weight=3];
5383[label="fromInt (Pos (Succ yu463) `quot` Neg (Succ yu464))\n  Integral a",fontsize=16,color="blue",shape="box"];5803[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];5383 -> 5803[label="",style="solid", color="blue", weight=9];
5803 -> 5397[label="",style="solid", color="blue", weight=3];
5804[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];5383 -> 5804[label="",style="solid", color="blue", weight=9];
5804 -> 5398[label="",style="solid", color="blue", weight=3];
1825[label="Integer (Pos Zero `quot` Neg (Succ yu78))",fontsize=16,color="green",shape="box"];1825 -> 1906[label="",style="dashed", color="green", weight=3];
1826[label="Pos Zero `quot` Neg (Succ yu78)",fontsize=16,color="black",shape="triangle"];1826 -> 1907[label="",style="solid", color="black", weight=3];
5341[label="floorN0 (Float (Neg (Succ yu449)) (Pos (Succ yu450))) (fromInt (Neg (Succ yu449) `quot` Pos (Succ yu450)),Float (Neg (Succ yu449)) (Pos (Succ yu450)) - fromInt (Neg (Succ yu449) `quot` Pos (Succ yu450)))\n  Integral a",fontsize=16,color="black",shape="box"];5341 -> 5357[label="",style="solid", color="black", weight=3];
5344[label="yu491",fontsize=16,color="green",shape="box"];2044[label="Integer (Neg Zero `quot` Pos (Succ yu87))",fontsize=16,color="green",shape="box"];2044 -> 2128[label="",style="dashed", color="green", weight=3];
2045[label="Neg Zero `quot` Pos (Succ yu87)",fontsize=16,color="black",shape="triangle"];2045 -> 2129[label="",style="solid", color="black", weight=3];
5384[label="fromInt (Neg (Succ yu468) `quot` Neg (Succ yu469))\n  Integral a",fontsize=16,color="blue",shape="box"];5805[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];5384 -> 5805[label="",style="solid", color="blue", weight=9];
5805 -> 5399[label="",style="solid", color="blue", weight=3];
5806[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];5384 -> 5806[label="",style="solid", color="blue", weight=9];
5806 -> 5400[label="",style="solid", color="blue", weight=3];
2254[label="Integer (Neg Zero `quot` Neg (Succ yu94))",fontsize=16,color="green",shape="box"];2254 -> 2280[label="",style="dashed", color="green", weight=3];
2255[label="Neg Zero `quot` Neg (Succ yu94)",fontsize=16,color="black",shape="triangle"];2255 -> 2281[label="",style="solid", color="black", weight=3];
3976[label="floorN0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (properFraction (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))))\n  Integral a",fontsize=16,color="black",shape="box"];3976 -> 4069[label="",style="solid", color="black", weight=3];
4489[label="error []",fontsize=16,color="red",shape="box"];4490 -> 2002[label="",style="dashed", color="red", weight=0];
4490[label="primMinusInt (floorN (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220)))) (fromInt (Pos (Succ Zero)))",fontsize=16,color="magenta"];4490 -> 4722[label="",style="dashed", color="magenta", weight=3];
4141 -> 2804[label="",style="dashed", color="red", weight=0];
4141[label="floorN (Float (Pos (Succ Zero)) (Pos (Succ yu283)))",fontsize=16,color="magenta"];2951[label="floorN0 (Float (Pos (Succ Zero)) (Pos (Succ yu283))) (fromInt (Pos (Succ Zero) `quot` Pos (Succ yu283)),Float (Pos (Succ Zero)) (Pos (Succ yu283)) - fromInt (Pos (Succ Zero) `quot` Pos (Succ yu283)))\n  Integral a",fontsize=16,color="black",shape="box"];2951 -> 2957[label="",style="solid", color="black", weight=3];
2048[label="primMinusNat (Succ yu19300) (Succ Zero)",fontsize=16,color="black",shape="box"];2048 -> 2227[label="",style="solid", color="black", weight=3];
2049[label="primMinusNat Zero (Succ Zero)",fontsize=16,color="black",shape="box"];2049 -> 2228[label="",style="solid", color="black", weight=3];
2050 -> 1596[label="",style="dashed", color="red", weight=0];
2050[label="primPlusNat yu1930 (Succ Zero)",fontsize=16,color="magenta"];2050 -> 2229[label="",style="dashed", color="magenta", weight=3];
1763 -> 1741[label="",style="dashed", color="red", weight=0];
1763[label="Pos Zero `quot` Pos (Succ yu71)",fontsize=16,color="magenta"];1764[label="primQuotInt (Pos Zero) (Pos (Succ yu71))",fontsize=16,color="black",shape="box"];1764 -> 2230[label="",style="solid", color="black", weight=3];
5397[label="fromInt (Pos (Succ yu463) `quot` Neg (Succ yu464))",fontsize=16,color="black",shape="box"];5397 -> 5450[label="",style="solid", color="black", weight=3];
5398[label="fromInt (Pos (Succ yu463) `quot` Neg (Succ yu464))",fontsize=16,color="black",shape="box"];5398 -> 5451[label="",style="solid", color="black", weight=3];
1906 -> 1826[label="",style="dashed", color="red", weight=0];
1906[label="Pos Zero `quot` Neg (Succ yu78)",fontsize=16,color="magenta"];1907[label="primQuotInt (Pos Zero) (Neg (Succ yu78))",fontsize=16,color="black",shape="box"];1907 -> 2335[label="",style="solid", color="black", weight=3];
5357[label="fromInt (Neg (Succ yu449) `quot` Pos (Succ yu450))\n  Integral a",fontsize=16,color="blue",shape="box"];5812[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];5357 -> 5812[label="",style="solid", color="blue", weight=9];
5812 -> 5372[label="",style="solid", color="blue", weight=3];
5813[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];5357 -> 5813[label="",style="solid", color="blue", weight=9];
5813 -> 5373[label="",style="solid", color="blue", weight=3];
2128 -> 2045[label="",style="dashed", color="red", weight=0];
2128[label="Neg Zero `quot` Pos (Succ yu87)",fontsize=16,color="magenta"];2129[label="primQuotInt (Neg Zero) (Pos (Succ yu87))",fontsize=16,color="black",shape="box"];2129 -> 2406[label="",style="solid", color="black", weight=3];
5399[label="fromInt (Neg (Succ yu468) `quot` Neg (Succ yu469))",fontsize=16,color="black",shape="box"];5399 -> 5452[label="",style="solid", color="black", weight=3];
5400[label="fromInt (Neg (Succ yu468) `quot` Neg (Succ yu469))",fontsize=16,color="black",shape="box"];5400 -> 5453[label="",style="solid", color="black", weight=3];
2280 -> 2255[label="",style="dashed", color="red", weight=0];
2280[label="Neg Zero `quot` Neg (Succ yu94)",fontsize=16,color="magenta"];2281[label="primQuotInt (Neg Zero) (Neg (Succ yu94))",fontsize=16,color="black",shape="box"];2281 -> 2456[label="",style="solid", color="black", weight=3];
4069[label="floorN0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (floatProperFractionFloat (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))))\n  Integral a",fontsize=16,color="black",shape="box"];4069 -> 4149[label="",style="solid", color="black", weight=3];
4722 -> 3927[label="",style="dashed", color="red", weight=0];
4722[label="floorN (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220)))",fontsize=16,color="magenta"];2957[label="fromInt (Pos (Succ Zero) `quot` Pos (Succ yu283))\n  Integral a",fontsize=16,color="blue",shape="box"];5817[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];2957 -> 5817[label="",style="solid", color="blue", weight=9];
5817 -> 2994[label="",style="solid", color="blue", weight=3];
5818[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];2957 -> 5818[label="",style="solid", color="blue", weight=9];
5818 -> 2995[label="",style="solid", color="blue", weight=3];
2227[label="primMinusNat yu19300 Zero",fontsize=16,color="burlywood",shape="triangle"];5819[label="yu19300/Succ yu193000",fontsize=10,color="white",style="solid",shape="box"];2227 -> 5819[label="",style="solid", color="burlywood", weight=9];
5819 -> 2522[label="",style="solid", color="burlywood", weight=3];
5820[label="yu19300/Zero",fontsize=10,color="white",style="solid",shape="box"];2227 -> 5820[label="",style="solid", color="burlywood", weight=9];
5820 -> 2523[label="",style="solid", color="burlywood", weight=3];
2228[label="Neg (Succ Zero)",fontsize=16,color="green",shape="box"];2229[label="yu1930",fontsize=16,color="green",shape="box"];2230[label="Pos (primDivNatS Zero (Succ yu71))",fontsize=16,color="green",shape="box"];2230 -> 2524[label="",style="dashed", color="green", weight=3];
5450[label="Integer (Pos (Succ yu463) `quot` Neg (Succ yu464))",fontsize=16,color="green",shape="box"];5450 -> 5459[label="",style="dashed", color="green", weight=3];
5451[label="Pos (Succ yu463) `quot` Neg (Succ yu464)",fontsize=16,color="black",shape="triangle"];5451 -> 5460[label="",style="solid", color="black", weight=3];
2335[label="Neg (primDivNatS Zero (Succ yu78))",fontsize=16,color="green",shape="box"];2335 -> 2569[label="",style="dashed", color="green", weight=3];
5372[label="fromInt (Neg (Succ yu449) `quot` Pos (Succ yu450))",fontsize=16,color="black",shape="box"];5372 -> 5385[label="",style="solid", color="black", weight=3];
5373[label="fromInt (Neg (Succ yu449) `quot` Pos (Succ yu450))",fontsize=16,color="black",shape="box"];5373 -> 5386[label="",style="solid", color="black", weight=3];
2406[label="Neg (primDivNatS Zero (Succ yu87))",fontsize=16,color="green",shape="box"];2406 -> 2635[label="",style="dashed", color="green", weight=3];
5452[label="Integer (Neg (Succ yu468) `quot` Neg (Succ yu469))",fontsize=16,color="green",shape="box"];5452 -> 5461[label="",style="dashed", color="green", weight=3];
5453[label="Neg (Succ yu468) `quot` Neg (Succ yu469)",fontsize=16,color="black",shape="triangle"];5453 -> 5462[label="",style="solid", color="black", weight=3];
2456[label="Pos (primDivNatS Zero (Succ yu94))",fontsize=16,color="green",shape="box"];2456 -> 2673[label="",style="dashed", color="green", weight=3];
4149[label="floorN0 (Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))) (fromInt (Pos (Succ (Succ yu2190)) `quot` Pos (Succ yu220)),Float (Pos (Succ (Succ yu2190))) (Pos (Succ yu220)) - fromInt (Pos (Succ (Succ yu2190)) `quot` Pos (Succ yu220)))\n  Integral a",fontsize=16,color="black",shape="box"];4149 -> 4230[label="",style="solid", color="black", weight=3];
2994[label="fromInt (Pos (Succ Zero) `quot` Pos (Succ yu283))",fontsize=16,color="black",shape="box"];2994 -> 3003[label="",style="solid", color="black", weight=3];
2995[label="fromInt (Pos (Succ Zero) `quot` Pos (Succ yu283))",fontsize=16,color="black",shape="box"];2995 -> 3004[label="",style="solid", color="black", weight=3];
2522[label="primMinusNat (Succ yu193000) Zero",fontsize=16,color="black",shape="box"];2522 -> 2777[label="",style="solid", color="black", weight=3];
2523[label="primMinusNat Zero Zero",fontsize=16,color="black",shape="box"];2523 -> 2778[label="",style="solid", color="black", weight=3];
5459 -> 5451[label="",style="dashed", color="red", weight=0];
5459[label="Pos (Succ yu463) `quot` Neg (Succ yu464)",fontsize=16,color="magenta"];5460[label="primQuotInt (Pos (Succ yu463)) (Neg (Succ yu464))",fontsize=16,color="black",shape="box"];5460 -> 5468[label="",style="solid", color="black", weight=3];
2569 -> 2524[label="",style="dashed", color="red", weight=0];
2569[label="primDivNatS Zero (Succ yu78)",fontsize=16,color="magenta"];2569 -> 2881[label="",style="dashed", color="magenta", weight=3];
5385[label="Integer (Neg (Succ yu449) `quot` Pos (Succ yu450))",fontsize=16,color="green",shape="box"];5385 -> 5401[label="",style="dashed", color="green", weight=3];
5386[label="Neg (Succ yu449) `quot` Pos (Succ yu450)",fontsize=16,color="black",shape="triangle"];5386 -> 5402[label="",style="solid", color="black", weight=3];
2635 -> 2524[label="",style="dashed", color="red", weight=0];
2635[label="primDivNatS Zero (Succ yu87)",fontsize=16,color="magenta"];2635 -> 2984[label="",style="dashed", color="magenta", weight=3];
5461 -> 5453[label="",style="dashed", color="red", weight=0];
5461[label="Neg (Succ yu468) `quot` Neg (Succ yu469)",fontsize=16,color="magenta"];5462[label="primQuotInt (Neg (Succ yu468)) (Neg (Succ yu469))",fontsize=16,color="black",shape="box"];5462 -> 5469[label="",style="solid", color="black", weight=3];
2673 -> 2524[label="",style="dashed", color="red", weight=0];
2673[label="primDivNatS Zero (Succ yu94)",fontsize=16,color="magenta"];2673 -> 3030[label="",style="dashed", color="magenta", weight=3];
4230[label="fromInt (Pos (Succ (Succ yu2190)) `quot` Pos (Succ yu220))\n  Integral a",fontsize=16,color="blue",shape="box"];5826[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];4230 -> 5826[label="",style="solid", color="blue", weight=9];
5826 -> 4258[label="",style="solid", color="blue", weight=3];
5827[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];4230 -> 5827[label="",style="solid", color="blue", weight=9];
5827 -> 4259[label="",style="solid", color="blue", weight=3];
3003[label="Integer (Pos (Succ Zero) `quot` Pos (Succ yu283))",fontsize=16,color="green",shape="box"];3003 -> 3528[label="",style="dashed", color="green", weight=3];
3004[label="Pos (Succ Zero) `quot` Pos (Succ yu283)",fontsize=16,color="black",shape="triangle"];3004 -> 3529[label="",style="solid", color="black", weight=3];
2777[label="Pos (Succ yu193000)",fontsize=16,color="green",shape="box"];2778[label="Pos Zero",fontsize=16,color="green",shape="box"];5468[label="Neg (primDivNatS (Succ yu463) (Succ yu464))",fontsize=16,color="green",shape="box"];5468 -> 5475[label="",style="dashed", color="green", weight=3];
2881[label="yu78",fontsize=16,color="green",shape="box"];5401 -> 5386[label="",style="dashed", color="red", weight=0];
5401[label="Neg (Succ yu449) `quot` Pos (Succ yu450)",fontsize=16,color="magenta"];5402[label="primQuotInt (Neg (Succ yu449)) (Pos (Succ yu450))",fontsize=16,color="black",shape="box"];5402 -> 5454[label="",style="solid", color="black", weight=3];
2984[label="yu87",fontsize=16,color="green",shape="box"];5469[label="Pos (primDivNatS (Succ yu468) (Succ yu469))",fontsize=16,color="green",shape="box"];5469 -> 5476[label="",style="dashed", color="green", weight=3];
3030[label="yu94",fontsize=16,color="green",shape="box"];4258[label="fromInt (Pos (Succ (Succ yu2190)) `quot` Pos (Succ yu220))",fontsize=16,color="black",shape="box"];4258 -> 4309[label="",style="solid", color="black", weight=3];
4259[label="fromInt (Pos (Succ (Succ yu2190)) `quot` Pos (Succ yu220))",fontsize=16,color="black",shape="box"];4259 -> 4310[label="",style="solid", color="black", weight=3];
3528 -> 3004[label="",style="dashed", color="red", weight=0];
3528[label="Pos (Succ Zero) `quot` Pos (Succ yu283)",fontsize=16,color="magenta"];3529[label="primQuotInt (Pos (Succ Zero)) (Pos (Succ yu283))",fontsize=16,color="black",shape="box"];3529 -> 3903[label="",style="solid", color="black", weight=3];
5475 -> 5463[label="",style="dashed", color="red", weight=0];
5475[label="primDivNatS (Succ yu463) (Succ yu464)",fontsize=16,color="magenta"];5475 -> 5480[label="",style="dashed", color="magenta", weight=3];
5475 -> 5481[label="",style="dashed", color="magenta", weight=3];
5454[label="Neg (primDivNatS (Succ yu449) (Succ yu450))",fontsize=16,color="green",shape="box"];5454 -> 5463[label="",style="dashed", color="green", weight=3];
5476 -> 5463[label="",style="dashed", color="red", weight=0];
5476[label="primDivNatS (Succ yu468) (Succ yu469)",fontsize=16,color="magenta"];5476 -> 5482[label="",style="dashed", color="magenta", weight=3];
5476 -> 5483[label="",style="dashed", color="magenta", weight=3];
4309[label="Integer (Pos (Succ (Succ yu2190)) `quot` Pos (Succ yu220))",fontsize=16,color="green",shape="box"];4309 -> 4480[label="",style="dashed", color="green", weight=3];
4310[label="Pos (Succ (Succ yu2190)) `quot` Pos (Succ yu220)",fontsize=16,color="black",shape="triangle"];4310 -> 4481[label="",style="solid", color="black", weight=3];
3903[label="Pos (primDivNatS (Succ Zero) (Succ yu283))",fontsize=16,color="green",shape="box"];3903 -> 4482[label="",style="dashed", color="green", weight=3];
5480[label="yu463",fontsize=16,color="green",shape="box"];5481[label="yu464",fontsize=16,color="green",shape="box"];5482[label="yu468",fontsize=16,color="green",shape="box"];5483[label="yu469",fontsize=16,color="green",shape="box"];4480 -> 4310[label="",style="dashed", color="red", weight=0];
4480[label="Pos (Succ (Succ yu2190)) `quot` Pos (Succ yu220)",fontsize=16,color="magenta"];4481[label="primQuotInt (Pos (Succ (Succ yu2190))) (Pos (Succ yu220))",fontsize=16,color="black",shape="box"];4481 -> 4979[label="",style="solid", color="black", weight=3];
4482[label="primDivNatS (Succ Zero) (Succ yu283)",fontsize=16,color="black",shape="box"];4482 -> 4980[label="",style="solid", color="black", weight=3];
4979[label="Pos (primDivNatS (Succ (Succ yu2190)) (Succ yu220))",fontsize=16,color="green",shape="box"];4979 -> 5092[label="",style="dashed", color="green", weight=3];
4980 -> 4878[label="",style="dashed", color="red", weight=0];
4980[label="primDivNatS0 Zero yu283 (primGEqNatS Zero yu283)",fontsize=16,color="magenta"];4980 -> 5093[label="",style="dashed", color="magenta", weight=3];
4980 -> 5094[label="",style="dashed", color="magenta", weight=3];
5092[label="primDivNatS (Succ (Succ yu2190)) (Succ yu220)",fontsize=16,color="black",shape="box"];5092 -> 5171[label="",style="solid", color="black", weight=3];
5093[label="yu283",fontsize=16,color="green",shape="box"];5094[label="Zero",fontsize=16,color="green",shape="box"];5171 -> 4878[label="",style="dashed", color="red", weight=0];
5171[label="primDivNatS0 (Succ yu2190) yu220 (primGEqNatS (Succ yu2190) yu220)",fontsize=16,color="magenta"];5171 -> 5277[label="",style="dashed", color="magenta", weight=3];
5171 -> 5278[label="",style="dashed", color="magenta", weight=3];
5277[label="yu220",fontsize=16,color="green",shape="box"];5278[label="Succ yu2190",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yu30000), Succ(yu47500)) → new_primPlusNat(yu30000, yu47500)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(yu30000), Succ(yu47500)) → new_primPlusNat(yu30000, yu47500)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(yu41400), Succ(yu43900)) → new_primMinusNat(yu41400, yu43900)

From the DPs we obtained the following set of size-change graphs:

new_primMinusNat(Succ(yu41400), Succ(yu43900)) → new_primMinusNat(yu41400, yu43900)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu497, yu498, Zero, Zero) → new_primDivNatS00(yu497, yu498)
new_primDivNatS1(yu449, yu450) → new_primDivNatS01(yu449, yu450)
new_primDivNatS01(Succ(yu30000), Zero) → new_primDivNatS02(yu30000)
new_primDivNatS02(yu30000) → new_primDivNatS(Succ(yu30000), Zero, Zero)
new_primDivNatS0(yu497, yu498, Succ(yu4990), Succ(yu5000)) → new_primDivNatS0(yu497, yu498, yu4990, yu5000)
new_primDivNatS(Succ(yu5020), Zero, yu504) → new_primDivNatS1(yu5020, yu504)
new_primDivNatS(Succ(yu5020), Succ(yu5030), yu504) → new_primDivNatS(yu5020, yu5030, yu504)
new_primDivNatS01(Succ(yu30000), Succ(yu31000)) → new_primDivNatS0(yu30000, yu31000, yu30000, yu31000)
new_primDivNatS00(yu497, yu498) → new_primDivNatS(Succ(yu497), Succ(yu498), Succ(yu498))
new_primDivNatS0(yu497, yu498, Succ(yu4990), Zero) → new_primDivNatS(Succ(yu497), Succ(yu498), Succ(yu498))
new_primDivNatS01(Zero, Zero) → new_primDivNatS03
new_primDivNatS03 → new_primDivNatS(Zero, Zero, Zero)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu497, yu498, Zero, Zero) → new_primDivNatS00(yu497, yu498)
new_primDivNatS02(yu30000) → new_primDivNatS(Succ(yu30000), Zero, Zero)
new_primDivNatS01(Succ(yu30000), Zero) → new_primDivNatS02(yu30000)
new_primDivNatS1(yu449, yu450) → new_primDivNatS01(yu449, yu450)
new_primDivNatS0(yu497, yu498, Succ(yu4990), Succ(yu5000)) → new_primDivNatS0(yu497, yu498, yu4990, yu5000)
new_primDivNatS(Succ(yu5020), Zero, yu504) → new_primDivNatS1(yu5020, yu504)
new_primDivNatS(Succ(yu5020), Succ(yu5030), yu504) → new_primDivNatS(yu5020, yu5030, yu504)
new_primDivNatS01(Succ(yu30000), Succ(yu31000)) → new_primDivNatS0(yu30000, yu31000, yu30000, yu31000)
new_primDivNatS00(yu497, yu498) → new_primDivNatS(Succ(yu497), Succ(yu498), Succ(yu498))
new_primDivNatS0(yu497, yu498, Succ(yu4990), Zero) → new_primDivNatS(Succ(yu497), Succ(yu498), Succ(yu498))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_primDivNatS(Succ(yu5020), Zero, yu504) → new_primDivNatS1(yu5020, yu504)
new_primDivNatS(Succ(yu5020), Succ(yu5030), yu504) → new_primDivNatS(yu5020, yu5030, yu504)

The remaining pairs can at least be oriented weakly.

new_primDivNatS0(yu497, yu498, Zero, Zero) → new_primDivNatS00(yu497, yu498)
new_primDivNatS02(yu30000) → new_primDivNatS(Succ(yu30000), Zero, Zero)
new_primDivNatS01(Succ(yu30000), Zero) → new_primDivNatS02(yu30000)
new_primDivNatS1(yu449, yu450) → new_primDivNatS01(yu449, yu450)
new_primDivNatS0(yu497, yu498, Succ(yu4990), Succ(yu5000)) → new_primDivNatS0(yu497, yu498, yu4990, yu5000)
new_primDivNatS01(Succ(yu30000), Succ(yu31000)) → new_primDivNatS0(yu30000, yu31000, yu30000, yu31000)
new_primDivNatS00(yu497, yu498) → new_primDivNatS(Succ(yu497), Succ(yu498), Succ(yu498))
new_primDivNatS0(yu497, yu498, Succ(yu4990), Zero) → new_primDivNatS(Succ(yu497), Succ(yu498), Succ(yu498))

Used ordering: Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 0
POL(new_primDivNatS(x₁, x₂, x₃)) = x₁
POL(new_primDivNatS0(x₁, x₂, x₃, x₄)) = 1 + x₁
POL(new_primDivNatS00(x₁, x₂)) = 1 + x₁
POL(new_primDivNatS01(x₁, x₂)) = x₁
POL(new_primDivNatS02(x₁)) = 1 + x₁
POL(new_primDivNatS1(x₁, x₂)) = x₁

The following usable rules [17] were oriented: none

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu497, yu498, Zero, Zero) → new_primDivNatS00(yu497, yu498)
new_primDivNatS1(yu449, yu450) → new_primDivNatS01(yu449, yu450)
new_primDivNatS01(Succ(yu30000), Zero) → new_primDivNatS02(yu30000)
new_primDivNatS02(yu30000) → new_primDivNatS(Succ(yu30000), Zero, Zero)
new_primDivNatS0(yu497, yu498, Succ(yu4990), Succ(yu5000)) → new_primDivNatS0(yu497, yu498, yu4990, yu5000)
new_primDivNatS01(Succ(yu30000), Succ(yu31000)) → new_primDivNatS0(yu30000, yu31000, yu30000, yu31000)
new_primDivNatS00(yu497, yu498) → new_primDivNatS(Succ(yu497), Succ(yu498), Succ(yu498))
new_primDivNatS0(yu497, yu498, Succ(yu4990), Zero) → new_primDivNatS(Succ(yu497), Succ(yu498), Succ(yu498))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 7 less nodes.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ QDPSizeChangeProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu497, yu498, Succ(yu4990), Succ(yu5000)) → new_primDivNatS0(yu497, yu498, yu4990, yu5000)

From the DPs we obtained the following set of size-change graphs:

new_primDivNatS0(yu497, yu498, Succ(yu4990), Succ(yu5000)) → new_primDivNatS0(yu497, yu498, yu4990, yu5000)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yu1120)) → new_primMulNat(yu1120)

From the DPs we obtained the following set of size-change graphs:

new_primMulNat(Succ(yu1120)) → new_primMulNat(yu1120)
The graph contains the following edges 1 > 1

primDivNatS0	x y True	= Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0	x y False	= Zero

primModNatS0	x y True	= primModNatS (primMinusNatS x y) (Succ y)
primModNatS0	x y False	= Succ x

floorFloor0	xx True	= floorN xx - 1
floorFloor0	xx False	= floorN xx